1  /-
  2  Copyright (c) 2017 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  
  6  Cofinality on ordinals, regular cardinals.
  7  -/
  8  import set_theory.ordinal
src         └────────────────┘
  9  noncomputable theory
 10  
 11  open function cardinal set
 12  open_locale classical
 13  
 14  universes u v w
 15  variables {α : Type*} {r : α → α → Prop}
 16  
 17  namespace order
 18  /-- Cofinality of a reflexive order `≼`. This is the smallest cardinality
 19    of a subset `S : set α` such that `∀ a, ∃ b ∈ S, a ≼ b`. -/
 20  def cof (r : α → α → Prop) [is_refl α r] : cardinal :=
id                             └─────┘      └──────┘
src                              └─────┘        └──────┘
typ                            └─────┘      └──────┘
doc                                             └──────┘
 21  @cardinal.min {S : set α // ∀ a, ∃ b ∈ S, r a b}
id    └──────────┘     └─┘                
src   └──────────┘     └─┘                 
typ   └──────────┘     └─┘                
doc   └──────────┘
 22    ⟨⟨set.univ, λ a, ⟨a, ⟨⟩, refl _⟩⟩⟩
id       └──────┘            └──┘
src      └──────┘              └──┘
typ      └──────┘            └──┘
 23    (λ S, mk S)
id          └┘ 
src          └┘
typ         └┘ 
doc          └┘
 24  
 25  lemma cof_le (r : α → α → Prop) [is_refl α r] {S : set α} (h : ∀a, ∃(b ∈ S), r a b) :
id                                  └─────┘         └─┘                   
src                                   └─────┘           └─┘                    
typ                                 └─────┘         └─┘                   
 26    order.cof r ≤ mk S :=
id     └───────┘   └┘ 
src    └───────┘    └┘
typ    └───────┘   └┘ 
doc    └───────┘     └┘
 27  le_trans (cardinal.min_le _ ⟨S, h⟩) (le_refl _)
id   └──────┘  └─────────────┘          └─────┘
src  └──────┘  └─────────────┘            └─────┘
typ  └──────┘  └─────────────┘          └─────┘
 28  
 29  lemma le_cof {r : α → α → Prop} [is_refl α r] (c : cardinal) :
id                                  └─────┘         └──────┘
src                                   └─────┘           └──────┘
typ                                 └─────┘         └──────┘
doc                                                     └──────┘
 30    c ≤ order.cof r ↔ ∀ {S : set α} (h : ∀a, ∃(b ∈ S), r a b) , c ≤ mk S :=
id       └───────┘          └─┘                         └┘ 
src       └───────┘           └─┘                                 └┘
typ      └───────┘          └─┘                         └┘ 
doc        └───────┘                                                   └┘
 31  by { rw [order.cof, cardinal.le_min], exact ⟨λ H S h, H ⟨S, h⟩, λ H ⟨S, h⟩, H h ⟩ }
id            └───────┘  └─────────────┘                                     
src       └──┘└───────┘└┘└─────────────┘  └────┘  └──────┘   └┘ └─┘ └──┘ └┘ └─┘  └─┘
typ       └──┘└───────┘└┘└─────────────┘  └────┘  └──────┘   └┘ └─┘ └──┘ └┘└─┘  └─┘
doc       └──┘└───────┘└┘                 └────┘  └──────┘   └┘ └─┘ └──┘ └┘ └─┘  └─┘
txt       └──┘         └┘                 └────┘  └──────┘   └┘ └─┘ └──┘ └┘ └─┘  └─┘
par       └──┘         └┘                 └────┘  └──────┘   └┘ └─┘ └──┘ └┘ └─┘  └─┘
pid         └┘         └┘                        └──────┘   └┘ └─┘ └──┘ └┘ └─┘  └┘
st     └──────────────┘└───────────────┘└─────────────────────────────────────────────┘└┘
 32  
 33  end order
 34  
 35  theorem order_iso.cof.aux {α : Type u} {β : Type v} {r s}
 36    [is_refl α r] [is_refl β s] (f : r ≃o s) :
id      └─────┘     └─────┘          └┘ 
src     └─────┘       └─────┘             └┘
typ     └─────┘     └─────┘          └┘ 
doc                                       └┘
 37    cardinal.lift.{u (max u v)} (order.cof r) ≤
id     └───────────┘                └───────┘   
src    └───────────┘                └───────┘    
typ    └───────────┘                └───────┘   
doc    └───────────┘                └───────┘
 38    cardinal.lift.{v (max u v)} (order.cof s) :=
id     └───────────┘                └───────┘ 
src    └───────────┘                └───────┘
typ    └───────────┘                └───────┘ 
doc    └───────────┘                └───────┘
 39  begin
st   └─────
 40    rw [order.cof, order.cof, lift_min, lift_min, cardinal.le_min],
id         └───────┘  └───────┘  └──────┘  └──────┘  └─────────────┘
src    └──┘└───────┘└┘└───────┘└┘└──────┘└┘└──────┘└┘└─────────────┘
typ    └──┘└───────┘└┘└───────┘└┘└──────┘└┘└──────┘└┘└─────────────┘
doc    └──┘└───────┘└┘└───────┘└┘        └┘        └┘               
txt    └──┘         └┘         └┘        └┘        └┘               
par    └──┘         └┘         └┘        └┘        └┘               
pid      └┘         └┘         └┘        └┘        └┘               
st   ──────────────┘└─────────┘└────────┘└────────┘└───────────────┘└──
 41    intro S, cases S with S H, simp [(∘)],
id                                     
src    └─────┘  └────┘ └───────┘  └────┘└─┘
typ    └─────┘  └────┘└───────┘  └────┘└─┘
doc    └─────┘  └────┘ └───────┘  └────┘ └─┘
txt    └─────┘  └────┘ └───────┘  └────┘ └─┘
par    └─────┘  └────┘ └───────┘  └────┘ └─┘
pid         └┘        └───────┘       └─┘
st   ────────┘└────────────────┘└──────────┘└─
 42    refine le_trans (min_le _ _) _,
id            └──────┘  └────┘
src    └─────┘└──────┘ └────┘└─────┘
typ    └─────┘└──────┘ └────┘└─────┘
doc    └─────┘               └─────┘
txt    └─────┘               └─────┘
par    └─────┘               └─────┘
pid                         └─────┘
st   ───────────────────────────────┘└─
 43    { exact ⟨f ⁻¹' S, λ a,
id                └─┘ 
src      └────┘  └─┘ └┘ └───
typ      └────┘  └─┘└┘ └───
doc      └────┘  └─┘ └┘ └───
txt      └────┘      └┘ └───
par      └────┘      └┘ └───
pid                 └┘ └───
st   ───┘└────────────────────
 44      let ⟨b, bS, h⟩ := H (f a) in ⟨f.symm b, by simp [bS, f.ord', h,
id                                  └────┘             └┘          
src  ───┘     └┘  └┘ └───┘    └───┘ └────┘ └┘  └────┘  └┘      └┘ └─
typ  ───┘    └┘  └┘ └───┘  └───┘ └────┘ └┘  └────┘└┘└┘└────┘└┘└─
doc  ───┘     └┘  └┘ └───┘    └───┘        └┘  └────┘  └┘      └┘ └─
txt  ───┘     └┘  └┘ └───┘    └───┘        └┘  └────┘  └┘      └┘ └─
par  ───┘     └┘  └┘ └───┘    └───┘        └┘  └────┘  └┘      └┘ └─
pid  ───┘     └┘  └┘ └───┘    └───┘        └┘  └─────┘  └┘      └┘ └─
st   ─────────────────────────────────────────────┘└─────────────────────
 45        -coe_fn_coe_base, -coe_fn_coe_trans, principal_seg.coe_coe_fn', initial_seg.coe_coe_fn]⟩⟩ },
id                                              └───────────────────────┘  └────────────────────┘
src  ──────────────────────────────────────────┘└───────────────────────┘└┘└────────────────────┘└─┘
typ  ──────────────────────────────────────────┘└───────────────────────┘└┘└────────────────────┘└─┘
doc  ──────────────────────────────────────────┘                         └┘                      └─┘
txt  ──────────────────────────────────────────┘                         └┘                      └─┘
par  ──────────────────────────────────────────┘                         └┘                      └─┘
pid  ──────────────────────────────────────────┘                         └┘                      └─┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─┘└┘
 46    { exact lift_mk_le.{u v (max u v)}.2
id             └────────┘
src      └────┘└────────┘└──────────────────
typ      └────┘└────────┘└──────────────────
doc      └────┘          └──────────────────
txt      └────┘          └──────────────────
par      └────┘          └──────────────────
pid                     └──────────────────
st   ───────────────────────────────────────
 47      ⟨⟨λ ⟨x, h⟩, ⟨f x, h⟩, λ ⟨x, h₁⟩ ⟨y, h₂⟩ h₃,
id                  
src  ───┘   └┘ └┘ └─┘   └┘ └─┘ └┘ └┘  └─┘ └┘  └─────
typ  ───┘   └┘└┘└─┘  └┘ └─┘ └┘ └┘  └─┘ └┘  └─────
doc  ───┘   └┘ └┘ └─┘   └┘ └─┘ └┘ └┘  └─┘ └┘  └─────
txt  ───┘   └┘ └┘ └─┘   └┘ └─┘ └┘ └┘  └─┘ └┘  └─────
par  ───┘   └┘ └┘ └─┘   └┘ └─┘ └┘ └┘  └─┘ └┘  └─────
pid  ───┘   └┘ └┘ └─┘   └┘ └─┘ └┘ └┘  └─┘ └┘  └─────
st   ────────────────────────────────────────────────
 48        by congr; injection h₃ with h'; exact f.to_equiv.injective h'⟩⟩ }
id                             └┘                └──────────────────┘ └┘
src  ─────┘  └───┘└┘└────────┘  └──────┘└──────┘└──────────────────┘  └─┘
typ  ─────┘  └───┘└┘└────────┘└┘└──────┘└──────┘└──────────────────┘└┘└─┘
doc  ─────┘       └┘└────────┘  └──────┘└──────┘                      └─┘
txt  ─────┘  └───┘└┘└────────┘  └──────┘└──────┘                      └─┘
par  ─────┘  └───┘└┘└────────┘  └──────┘└──────┘                      └─┘
pid  ─────┘  └────────────────┘  └──────────────┘                      └┘
st   ───────┘└─────────────────────────────────────────────────────────┘└─┘└─
 49  end
st   ──┘
 50  
 51  theorem order_iso.cof {α : Type u} {β : Type v} {r s}
 52    [is_refl α r] [is_refl β s] (f : r ≃o s) :
id      └─────┘     └─────┘          └┘ 
src     └─────┘       └─────┘             └┘
typ     └─────┘     └─────┘          └┘ 
doc                                       └┘
 53    cardinal.lift.{u (max u v)} (order.cof r) =
id     └───────────┘                └───────┘   
src    └───────────┘                └───────┘    
typ    └───────────┘                └───────┘   
doc    └───────────┘                └───────┘
 54    cardinal.lift.{v (max u v)} (order.cof s) :=
id     └───────────┘                └───────┘ 
src    └───────────┘                └───────┘
typ    └───────────┘                └───────┘ 
doc    └───────────┘                └───────┘
 55  le_antisymm (order_iso.cof.aux f) (order_iso.cof.aux f.symm)
id   └─────────┘  └───────────────┘    └───────────────┘ └───┘
src  └─────────┘  └───────────────┘     └───────────────┘  └───┘
typ  └─────────┘  └───────────────┘    └───────────────┘ └───┘
 56  
 57  def strict_order.cof (r : α → α → Prop) [h : is_irrefl α r] : cardinal :=
id                                              └───────┘      └──────┘
src                                               └───────┘        └──────┘
typ                                             └───────┘      └──────┘
doc                                                                └──────┘
 58  @order.cof α (λ x y, ¬ r y x) ⟨h.1⟩
id    └───────┘              
src   └───────┘                     
typ   └───────┘              
doc   └───────┘
 59  
 60  namespace ordinal
 61  
 62  /-- Cofinality of an ordinal. This is the smallest cardinal of a
 63    subset `S` of the ordinal which is unbounded, in the sense
 64    `∀ a, ∃ b ∈ S, ¬(b > a)`. It is defined for all ordinals, but
 65    `cof 0 = 0` and `cof (succ o) = 1`, so it is only really
 66    interesting on limit ordinals (when it is an infinite cardinal). -/
 67  def cof (o : ordinal.{u}) : cardinal.{u} :=
id                └─────┘        └──────┘
src               └─────┘        └──────┘
typ               └─────┘        └──────┘
doc               └─────┘        └──────┘
 68  quot.lift_on o (λ ⟨α, r, _⟩, by exactI strict_order.cof r) $
id   └──────────┘                         └──────────────┘ 
src  └──────────┘                    └─────┘└──────────────┘
typ  └──────────┘                  └─────┘└──────────────┘
doc                                  └─────┘                
txt                                  └─────┘                
par                                  └─────┘                
pid                                                        
st                                  └────────────────────────┘
 69  λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨⟨f, hf⟩⟩, begin resetI,
id                       
src                                         └────┘
typ                                      └────┘
doc                                         └────┘
txt                                         └────┘
par                                         └────┘
st                                    └─────────────
 70    show strict_order.cof r = strict_order.cof s,
id                             └──────────────┘ 
src    └───┘                 └──────────────┘
typ    └───┘                └──────────────┘
doc    └───┘                                  
txt    └───┘                                  
par    └───┘                                  
pid    └───┘                                  
st   ─────────────────────────────────────────────┘└─
 71    refine cardinal.lift_inj.1 (@order_iso.cof _ _ _ _ ⟨_⟩ ⟨_⟩ _),
id            └───────────────┘     └───────────┘
src    └─────┘└───────────────┘└─┘  └───────────┘└───────┘ └─┘ └───┘
typ    └─────┘└───────────────┘└─┘  └───────────┘└───────┘ └─┘ └───┘
doc    └─────┘                 └─┘               └───────┘ └─┘ └───┘
txt    └─────┘                 └─┘               └───────┘ └─┘ └───┘
par    └─────┘                 └─┘               └───────┘ └─┘ └───┘
pid                           └─┘               └───────┘ └─┘ └───┘
st   ──────────────────────────────────────────────────────────────┘└─
 72    exact ⟨f, λ a b, not_congr hf⟩,
id                     └───────┘ └┘
src    └────┘  └┘ └────┘└───────┘  
typ    └────┘ └┘ └────┘└───────┘└┘
doc    └────┘  └┘ └────┘           
txt    └────┘  └┘ └────┘           
par    └────┘  └┘ └────┘           
pid           └┘ └────┘           
st   ───────────────────────────────┘└─
 73  end
st   ──┘
 74  
 75  lemma cof_type (r : α → α → Prop) [is_well_order α r] : (type r).cof = strict_order.cof r := rfl
id                                    └───────────┘       └──┘  └─┘   └──────────────┘     └─┘
src                                     └───────────┘         └──┘   └─┘   └──────────────┘      └─┘
typ                                   └───────────┘       └──┘  └─┘   └──────────────┘     └─┘
doc                                     └───────────┘         └──┘   └─┘
 76  
 77  theorem le_cof_type [is_well_order α r] {c} : c ≤ cof (type r) ↔
id                        └───────────┘            └─┘  └──┘   
src                       └───────────┘               └─┘  └──┘    
typ                       └───────────┘            └─┘  └──┘   
doc                       └───────────┘                └─┘  └──┘
 78    ∀ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) → c ≤ mk S :=
id           └─┘                      └┘ 
src          └─┘                              └┘
typ          └─┘                      └┘ 
doc                                               └┘
 79  by dsimp [cof, strict_order.cof, order.cof, type, quotient.mk, quot.lift_on];
id             └─┘  └──────────────┘  └───────┘  └──┘  └─────────┘  └──────────┘
src     └─────┘└─┘└┘└──────────────┘└┘└───────┘└┘└──┘└┘└─────────┘└┘└──────────┘
typ     └─────┘└─┘└┘└──────────────┘└┘└───────┘└┘└──┘└┘└─────────┘└┘└──────────┘
doc     └─────┘└─┘└┘                └┘└───────┘└┘└──┘└┘           └┘            
txt     └─────┘   └┘                └┘         └┘    └┘           └┘            
par     └─────┘   └┘                └┘         └┘    └┘           └┘            
pid             └┘                └┘         └┘    └┘           └┘            
st     └───────────────────────────────────────────────────────────────────────────
 80     rw [cardinal.le_min, subtype.forall]; refl
id          └─────────────┘  └────────────┘
src     └──┘└─────────────┘└┘└────────────┘  └────
typ     └──┘└─────────────┘└┘└────────────┘  └────
doc     └──┘               └┘                └────
txt     └──┘               └┘                └────
par     └──┘               └┘                └────
pid       └┘               └┘                    
st   ──────┘└─────────────┘└──────────────┘└──────
 81  
src  
typ  
doc  
txt  
par  
pid  
st   
 82  theorem cof_type_le [is_well_order α r] (S : set α) (h : ∀ a, ∃ b ∈ S, ¬ r b a) :
id                        └───────────┘         └─┘                    
src                       └───────────┘           └─┘                     
typ                       └───────────┘         └─┘                    
doc                       └───────────┘
 83    cof (type r) ≤ mk S :=
id     └─┘  └──┘    └┘ 
src    └─┘  └──┘     └┘
typ    └─┘  └──┘    └┘ 
doc    └─┘  └──┘      └┘
 84  le_cof_type.1 (le_refl _) S h
id   └─────────┘   └─────┘     
src  └─────────┘   └─────┘
typ  └─────────┘   └─────┘     
 85  
 86  theorem lt_cof_type [is_well_order α r] (S : set α) (hl : mk S < cof (type r)) :
id                        └───────────┘         └─┘         └┘   └─┘  └──┘ 
src                       └───────────┘           └─┘          └┘    └─┘  └──┘
typ                       └───────────┘         └─┘         └┘   └─┘  └──┘ 
doc                       └───────────┘                        └┘     └─┘  └──┘
 87    ∃ a, ∀ b ∈ S, r b a :=
id                
src         
typ               
 88  not_forall_not.1 $ λ h, not_le_of_lt hl $ cof_type_le S (λ a, not_ball.1 (h a))
id   └────────────┘        └──────────┘ └┘   └─────────┘       └──────┘    
src  └────────────┘         └──────────┘      └─────────┘         └──────┘
typ  └────────────┘        └──────────┘ └┘   └─────────┘       └──────┘    
 89  
 90  theorem cof_eq (r : α → α → Prop) [is_well_order α r] :
id                                    └───────────┘  
src                                     └───────────┘
typ                                   └───────────┘  
doc                                     └───────────┘
 91    ∃ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) ∧ mk S = cof (type r) :=
id          └─┘                  └┘   └─┘  └──┘ 
src         └─┘                         └┘    └─┘  └──┘
typ         └─┘                  └┘   └─┘  └──┘ 
doc                                           └┘     └─┘  └──┘
 92  begin
st   └─────
 93    have : ∃ i, cof (type r) = _,
id               └─┘  └──┘   
src    └─────┘└┘└─┘ └──┘ └┘└┘
typ    └─────┘└┘└─┘ └──┘└┘└┘
doc    └─────┘ └┘ └─┘ └──┘ └┘ └┘
txt    └─────┘ └┘          └┘ └┘
par    └─────┘ └┘          └┘ └┘
pid    └───┘└┘ └┘          └┘ └┘
st   ─────────────────────────────┘└─
 94    { dsimp [cof, order.cof, type, quotient.mk, quot.lift_on],
id              └─┘  └───────┘  └──┘  └─────────┘  └──────────┘
src      └─────┘└─┘└┘└───────┘└┘└──┘└┘└─────────┘└┘└──────────┘
typ      └─────┘└─┘└┘└───────┘└┘└──┘└┘└─────────┘└┘└──────────┘
doc      └─────┘└─┘└┘└───────┘└┘└──┘└┘           └┘            
txt      └─────┘   └┘         └┘    └┘           └┘            
par      └─────┘   └┘         └┘    └┘           └┘            
pid              └┘         └┘    └┘           └┘            
st   ───┘└─────────────────────────────────────────────────────┘└─
 95      apply cardinal.min_eq },
id             └─────────────┘
src      └────┘└─────────────┘
typ      └────┘└─────────────┘
doc      └────┘               
txt      └────┘               
par      └────┘               
pid                          
st   ─────────────────────────┘└┘
 96    exact let ⟨⟨S, hl⟩, e⟩ := this in ⟨S, hl, e.symm⟩,
id                   └┘        └──┘             └───┘
src    └────┘      └┘  └─┘ └───┘    └──┘  └┘  └┘ └───┘
typ    └────┘     └┘└┘└─┘└───┘└──┘└──┘  └┘  └┘ └───┘
doc    └────┘      └┘  └─┘ └───┘    └──┘  └┘  └┘      
txt    └────┘      └┘  └─┘ └───┘    └──┘  └┘  └┘      
par    └────┘      └┘  └─┘ └───┘    └──┘  └┘  └┘      
pid               └┘  └─┘ └───┘    └──┘  └┘  └┘      
st   ──────────────────────────────────────────────────┘└─
 97  end
st   ──┘
 98  
 99  theorem ord_cof_eq (r : α → α → Prop) [is_well_order α r] :
id                                        └───────────┘  
src                                         └───────────┘
typ                                       └───────────┘  
doc                                         └───────────┘
100    ∃ S : set α, (∀ a, ∃ b ∈ S, ¬ r b a) ∧ type (subrel r S) = (cof (type r)).ord :=
id          └─┘                  └──┘  └────┘      └─┘  └──┘   └─┘
src         └─┘                         └──┘  └────┘        └─┘  └──┘    └─┘
typ         └─┘                  └──┘  └────┘      └─┘  └──┘   └─┘
doc                                           └──┘  └────┘         └─┘  └──┘    └─┘
101  let ⟨S, hS, e⟩ := cof_eq r, ⟨s, _, e'⟩ := cardinal.ord_eq S,
id   └─┘              └────┘                └─────────────┘
src                    └────┘                  └─────────────┘
typ  └─┘              └────┘                └─────────────┘
102      T : set α := {a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a} in
id           └─┘                                 └┘      
src          └─┘                    
typ          └─┘                                 └┘      
103  begin
st   └─────
104    resetI, suffices,
src    └────┘  └──────┘
typ    └────┘  └──────┘
doc    └────┘  └──────┘
txt    └────┘  └──────┘
par    └────┘  └──────┘
pid            └──────┘
st   ─────────────────┘└─
105    { refine ⟨T, this,
src      └─────┘  └┘    └─
typ      └─────┘  └┘    └─
doc      └─────┘  └┘    └─
txt      └─────┘  └┘    └─
par      └─────┘  └┘    └─
pid              └┘    └─
st   ───┘└────────────────
106        le_antisymm _ (cardinal.ord_le.2 $ cof_type_le T this)⟩,
id         └─────────┘    └─────────────┘     └─────────┘  └──┘
src  ─────┘└─────────┘└─┘ └─────────────┘└─┘ └─────────┘     └┘
typ  ─────┘└─────────┘└─┘ └─────────────┘└─┘ └─────────┘└──┘└┘
doc  ─────┘           └─┘                └─┘                 └┘
txt  ─────┘           └─┘                └─┘                 └┘
par  ─────┘           └─┘                └─┘                 └┘
pid  ─────┘           └─┘                └─┘                 └┘
st   ────────────────────────────────────────────────────────────┘└─
107      rw [← e, e'],
id               └┘
src      └────┘ └┘  
typ      └────┘└┘└┘
doc      └────┘ └┘  
txt      └────┘ └┘  
par      └────┘ └┘  
pid        └──┘ └┘  
st   ──────────┘└──┘└──
108      refine type_le'.2 ⟨order_embedding.of_monotone
id              └──────┘    └─────────────────────────┘
src      └─────┘└──────┘└─┘ └─────────────────────────┘
typ      └─────┘└──────┘└─┘ └─────────────────────────┘
doc      └─────┘        └─┘ └─────────────────────────┘
txt      └─────┘        └─┘                            
par      └─────┘        └─┘                            
pid                    └─┘                            
st   ───────────────────────────────────────────────────
109        (λ a, ⟨a, let ⟨aS, _⟩ := a.2 in aS⟩) (λ a b h, _)⟩,
id                        └┘
src  ─────┘  └──┘  └┘      └──────┘ └────┘  └─┘  └─────────┘
typ  ─────┘  └──┘  └┘    └┘└──────┘ └────┘  └─┘  └─────────┘
doc  ─────┘  └──┘  └┘      └──────┘ └────┘  └─┘  └─────────┘
txt  ─────┘  └──┘  └┘      └──────┘ └────┘  └─┘  └─────────┘
par  ─────┘  └──┘  └┘      └──────┘ └────┘  └─┘  └─────────┘
pid  ─────┘  └──┘  └┘      └──────┘ └────┘  └─┘  └─────────┘
st   ───────────────────────────────────────────────────────┘└─
110      rcases a with ⟨a, aS, ha⟩, rcases b with ⟨b, bS, hb⟩,
id                                        
src      └─────┘ └───────────────┘  └─────┘ └───────────────┘
typ      └─────┘└───────────────┘  └─────┘└───────────────┘
doc      └─────┘ └───────────────┘  └─────┘ └───────────────┘
txt      └─────┘ └───────────────┘  └─────┘ └───────────────┘
par      └─────┘ └───────────────┘  └─────┘ └───────────────┘
pid             └───────────────┘         └───────────────┘
st   ────────────────────────────┘└─────────────────────────┘└─
111      change s ⟨a, _⟩ ⟨b, _⟩,
id                      
src      └─────┘   └───┘  └──┘
typ      └─────┘ └───┘ └──┘
doc      └─────┘   └───┘  └──┘
txt      └─────┘   └───┘  └──┘
par      └─────┘   └───┘  └──┘
pid               └───┘  └──┘
st   ─────────────────────────┘└─
112      refine ((trichotomous_of s _ _).resolve_left (λ hn, _)).resolve_left _,
id                └─────────────┘ 
src      └─────┘  └─────────────┘ └─────────────────┘  └─────────────────────┘
typ      └─────┘  └─────────────┘└─────────────────┘  └─────────────────────┘
doc      └─────┘                  └─────────────────┘  └─────────────────────┘
txt      └─────┘                  └─────────────────┘  └─────────────────────┘
par      └─────┘                  └─────────────────┘  └─────────────────────┘
pid                              └─────────────────┘  └─────────────────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
113      { exact asymm h (ha _ hn) },
id               └───┘   └┘   └┘
src        └────┘└───┘    └─┘  └┘
typ        └────┘└───┘ └┘└─┘└┘└┘
doc        └────┘         └─┘  └┘
txt        └────┘         └─┘  └┘
par        └────┘         └─┘  └┘
pid                      └─┘  
st   ─────┘└──────────────────────┘└┘
114      { intro e, injection e with e, subst b,
id                                           
src        └─────┘  └────────┘ └─────┘  └────┘
typ        └─────┘  └────────┘└─────┘  └────┘
doc        └─────┘  └────────┘ └─────┘  └────┘
txt        └─────┘  └────────┘ └─────┘  └────┘
par        └─────┘  └────────┘ └─────┘  └────┘
pid             └┘            └─────┘       
st   ────────────┘└──────────────────┘└───────┘└─
115        exact irrefl _ h } },
id               └────┘   
src        └────┘└────┘└─┘ 
typ        └────┘└────┘└─┘
doc        └────┘      └─┘ 
txt        └────┘      └─┘ 
par        └────┘      └─┘ 
pid                   └─┘ 
st   ──────────────────────┘└──┘
116    { intro a,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ──────────┘└─
117      have : {b : S | ¬ r b a}.nonempty := let ⟨b, bS, ba⟩ := hS a in ⟨⟨b, bS⟩, ba⟩,
id                                               └┘  └┘     └┘ 
src      └─────┘└──┘ └─┘    └────────────┘     └┘  └┘  └───┘   └──┘   └┘  └─┘  
typ      └─────┘└──┘└─┘  └────────────┘    └┘└┘└┘└┘└───┘└┘└──┘   └┘  └─┘  
doc      └─────┘ └──┘ └─┘    └────────────┘     └┘  └┘  └───┘   └──┘   └┘  └─┘  
txt      └─────┘ └──┘ └─┘    └────────────┘     └┘  └┘  └───┘   └──┘   └┘  └─┘  
par      └─────┘ └──┘ └─┘    └────────────┘     └┘  └┘  └───┘   └──┘   └┘  └─┘  
pid      └───┘└┘ └──┘ └─┘    └───────┘└───┘     └┘  └┘  └───┘   └──┘   └┘  └─┘  
st   ────────────────────────────────────────────────────────────────────────────────┘└─
118      let b := (is_well_order.wf s).min _ this,
id                 └──────────────┘         └──┘
src      └───────┘ └──────────────┘ └──────┘
typ      └───────┘ └──────────────┘└──────┘└──┘
doc      └───────┘                  └──────┘
txt      └───────┘                  └──────┘
par      └───────┘                  └──────┘
pid      └───┘└─┘                  └──────┘
st   ───────────────────────────────────────────┘└─
119      have ba : ¬r b a := (is_well_order.wf s).min_mem _ this,
id                         └──────────────┘             └──┘
src      └────────┘    └──┘ └──────────────┘ └──────────┘
typ      └────────┘ └──┘ └──────────────┘└──────────┘└──┘
doc      └────────┘    └──┘                  └──────────┘
txt      └────────┘    └──┘                  └──────────┘
par      └────────┘    └──┘                  └──────────┘
pid      └─────┘└─┘    └──┘                  └──────────┘
st   ──────────────────────────────────────────────────────────┘└─
120      refine ⟨b, ⟨b.2, λ c, not_imp_not.1 $ λ h, _⟩, ba⟩,
id                            └─────────┘              └┘
src      └─────┘  └┘  └──┘ └──┘└─────────┘└─┘  └──────┘  
typ      └─────┘  └┘ └──┘ └──┘└─────────┘└─┘  └──────┘└┘
doc      └─────┘  └┘  └──┘ └──┘           └─┘  └──────┘  
txt      └─────┘  └┘  └──┘ └──┘           └─┘  └──────┘  
par      └─────┘  └┘  └──┘ └──┘           └─┘  └──────┘  
pid              └┘  └──┘ └──┘           └─┘  └──────┘  
st   ─────────────────────────────────────────────────────┘└─
121      rw [show ∀b:S, (⟨b, b.2⟩:S) = b, by intro b; cases b; refl],
id                                                        
src      └──┘     └┘     └┘ └──┘ └┘ └───┘└─────┘└┘└────┘ └┘└──┘
typ      └──┘     └┘     └┘ └──┘└┘ └───┘└─────┘└┘└────┘└┘└──┘
doc      └──┘     └┘     └┘ └──┘ └┘  └───┘└─────┘└┘└────┘ └┘└──┘
txt      └──┘     └┘     └┘ └──┘ └┘  └───┘└─────┘└┘└────┘ └┘└──┘
par      └──┘     └┘     └┘ └──┘ └┘  └───┘└─────┘└┘└────┘ └┘└──┘
pid        └┘     └┘     └┘ └──┘ └┘  └──────────────────┘ └─────┘
st   ──────────────────────────────────────┘└─────────────────────┘└──
122      exact (is_well_order.wf s).not_lt_min _ this
id              └──────────────┘                └──┘
src      └────┘ └──────────────┘ └─────────────┘    
typ      └────┘ └──────────────┘└─────────────┘└──┘
doc      └────┘                  └─────────────┘    
txt      └────┘                  └─────────────┘    
par      └────┘                  └─────────────┘    
pid                             └─────────────┘    
st   ─────────────────────────────────────────────────
123        (is_order_connected.neg_trans h ba) }
id          └──────────────────────────┘  └┘
src  ─────┘ └──────────────────────────┘   └┘
typ  ─────┘ └──────────────────────────┘└┘└┘
doc  ─────┘                                └┘
txt  ─────┘                                └┘
par  ─────┘                                └┘
pid  ─────┘                                
st   ─────────────────────────────────────────┘└─
124  end
st   ──┘
125  
126  theorem lift_cof (o) : (cof o).lift = cof o.lift :=
id                           └─┘  └──┘   └─┘ └───┘
src                          └─┘   └──┘   └─┘  └───┘
typ                          └─┘  └──┘   └─┘ └───┘
doc                          └─┘   └──┘    └─┘  └───┘
127  induction_on o $ begin introsI α r _,
id   └──────────┘ 
src  └──────────┘           └───────────┘
typ  └──────────┘          └───────────┘
doc                         └───────────┘
txt                         └───────────┘
par                         └───────────┘
pid                                └────┘
st                    └─────────────────┘└─
128    cases lift_type r with _ e, rw e,
id           └───────┘               
src    └────┘└───────┘ └───────┘  └─┘
typ    └────┘└───────┘└───────┘  └─┘
doc    └────┘          └───────┘  └─┘
txt    └────┘          └───────┘  └─┘
par    └────┘          └───────┘  └─┘
pid                   └───────┘    
st   ───────────────────────────┘└────┘└─
129    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
130    { refine le_cof_type.2 (λ S H, _),
id              └─────────┘
src      └─────┘└─────────┘└─┘  └──────┘
typ      └─────┘└─────────┘└─┘  └──────┘
doc      └─────┘           └─┘  └──────┘
txt      └─────┘           └─┘  └──────┘
par      └─────┘           └─┘  └──────┘
pid                       └─┘  └──────┘
st   ───┘└─────────────────────────────┘└─
131      have : (mk (ulift.up ⁻¹' S)).lift ≤ mk S :=
id                   └──────┘ └─┘           └┘ 
src      └─────┘    └──────┘└─┘ └──────┘└┘ └───
typ      └─────┘    └──────┘└─┘ └──────┘└┘└───
doc      └─────┘            └─┘ └──────┘ └┘ └───
txt      └─────┘                └──────┘    └───
par      └─────┘                └──────┘    └───
pid      └───┘└┘                └──────┘    └───
st   ────────────────────────────────────────────────
132       ⟨⟨λ ⟨⟨x, h⟩⟩, ⟨⟨x⟩, h⟩,
id                
src  ────┘   └┘  └┘ └──┘   └─┘ └──
typ  ────┘   └┘ └┘└──┘   └─┘ └──
doc  ────┘   └┘  └┘ └──┘   └─┘ └──
txt  ────┘   └┘  └┘ └──┘   └─┘ └──
par  ────┘   └┘  └┘ └──┘   └─┘ └──
pid  ────┘   └┘  └┘ └──┘   └─┘ └──
st   ─────────────────────────────
133         λ ⟨⟨x, h₁⟩⟩ ⟨⟨y, h₂⟩⟩ e, by simp at e; congr; injection e⟩⟩,
id                                                                  
src  ──────┘ └┘  └┘  └──┘  └┘  └────┘  └───────┘└┘└───┘└┘└────────┘ └┘
typ  ──────┘ └┘  └┘  └──┘  └┘  └────┘  └───────┘└┘└───┘└┘└────────┘└┘
doc  ──────┘ └┘  └┘  └──┘  └┘  └────┘  └───────┘└┘     └┘└────────┘ └┘
txt  ──────┘ └┘  └┘  └──┘  └┘  └────┘  └───────┘└┘└───┘└┘└────────┘ └┘
par  ──────┘ └┘  └┘  └──┘  └┘  └────┘  └───────┘└┘└───┘└┘└────────┘ └┘
pid  ──────┘ └┘  └┘  └──┘  └┘  └────┘  └───────────────────────────┘ └┘
st   ─────────────────────────────────┘└────────────────────────────┘└┘└─
134      refine le_trans (cardinal.lift_le.2 $ cof_type_le _ _) this,
id              └──────┘  └──────────────┘     └─────────┘      └──┘
src      └─────┘└──────┘ └──────────────┘└─┘ └─────────┘└────┘
typ      └─────┘└──────┘ └──────────────┘└─┘ └─────────┘└────┘└──┘
doc      └─────┘                         └─┘            └────┘
txt      └─────┘                         └─┘            └────┘
par      └─────┘                         └─┘            └────┘
pid                                     └─┘            └────┘
st   ──────────────────────────────────────────────────────────────┘└─
135      exact λ a, let ⟨⟨b⟩, bs, br⟩ := H ⟨a⟩ in ⟨b, bs, br⟩ },
id                           └┘  └┘     
src      └────┘ └──┘      └─┘  └┘  └───┘   └───┘  └┘  └┘  └┘
typ      └────┘ └──┘     └─┘└┘└┘└┘└───┘  └───┘  └┘  └┘  └┘
doc      └────┘ └──┘      └─┘  └┘  └───┘   └───┘  └┘  └┘  └┘
txt      └────┘ └──┘      └─┘  └┘  └───┘   └───┘  └┘  └┘  └┘
par      └────┘ └──┘      └─┘  └┘  └───┘   └───┘  └┘  └┘  └┘
pid            └──┘      └─┘  └┘  └───┘   └───┘  └┘  └┘  
st   ────────────────────────────────────────────────────────┘└┘
136    { rcases cof_eq r with ⟨S, H, e'⟩,
id              └────┘ 
src      └─────┘└────┘ └──────────────┘
typ      └─────┘└────┘└──────────────┘
doc      └─────┘       └──────────────┘
txt      └─────┘       └──────────────┘
par      └─────┘       └──────────────┘
pid                   └──────────────┘
st   ──────────────────────────────────┘└─
137      have : mk (ulift.down ⁻¹' S) ≤ (mk S).lift :=
id                  └────────┘           └┘ 
src      └─────┘   └────────┘    └┘  └┘ └─────────
typ      └─────┘   └────────┘    └┘  └┘└─────────
doc      └─────┘                 └┘  └┘ └─────────
txt      └─────┘                 └┘     └─────────
par      └─────┘                 └┘     └─────────
pid      └───┘└┘                 └┘     └───┘└────
st   ──────────────────────────────────────────────────
138       ⟨⟨λ ⟨⟨x⟩, h⟩, ⟨⟨x, h⟩⟩,
id                 
src  ────┘   └┘  └─┘ └─┘   └┘ └───
typ  ────┘   └┘ └─┘└─┘   └┘ └───
doc  ────┘   └┘  └─┘ └─┘   └┘ └───
txt  ────┘   └┘  └─┘ └─┘   └┘ └───
par  ────┘   └┘  └─┘ └─┘   └┘ └───
pid  ────┘   └┘  └─┘ └─┘   └┘ └───
st   ─────────────────────────────
139         λ ⟨⟨x⟩, h₁⟩ ⟨⟨y⟩, h₂⟩ e, by simp at e; congr; injections⟩⟩,
src  ──────┘ └┘  └─┘  └─┘  └─┘  └───┘  └───────┘└┘└───┘└┘└────────┘└┘
typ  ──────┘ └┘  └─┘  └─┘  └─┘  └───┘  └───────┘└┘└───┘└┘└────────┘└┘
doc  ──────┘ └┘  └─┘  └─┘  └─┘  └───┘  └───────┘└┘     └┘└────────┘└┘
txt  ──────┘ └┘  └─┘  └─┘  └─┘  └───┘  └───────┘└┘└───┘└┘└────────┘└┘
par  ──────┘ └┘  └─┘  └─┘  └─┘  └───┘  └───────┘└┘└───┘└┘└────────┘└┘
pid  ──────┘ └┘  └─┘  └─┘  └─┘  └───┘  └─────────────────────────────┘
st   ─────────────────────────────────┘└───────────────────────────┘└┘└─
140      rw e' at this,
id          └┘
src      └─┘  └──────┘
typ      └─┘└┘└──────┘
doc      └─┘  └──────┘
txt      └─┘  └──────┘
par      └─┘  └──────┘
pid          └──────┘
st   ────────────────┘└─
141      refine le_trans (cof_type_le _ _) this,
id              └──────┘  └─────────┘      └──┘
src      └─────┘└──────┘ └─────────┘└────┘
typ      └─────┘└──────┘ └─────────┘└────┘└──┘
doc      └─────┘                    └────┘
txt      └─────┘                    └────┘
par      └─────┘                    └────┘
pid                                └────┘
st   ─────────────────────────────────────────┘└─
142      exact λ ⟨a⟩, let ⟨b, bs, br⟩ := H a in ⟨⟨b⟩, bs, br⟩ }
id                          └┘  └┘     
src      └────┘ └┘ └─┘     └┘  └┘  └───┘  └──┘   └─┘  └┘  └┘
typ      └────┘ └┘└─┘    └┘└┘└┘└┘└───┘ └──┘   └─┘  └┘  └┘
doc      └────┘ └┘ └─┘     └┘  └┘  └───┘  └──┘   └─┘  └┘  └┘
txt      └────┘ └┘ └─┘     └┘  └┘  └───┘  └──┘   └─┘  └┘  └┘
par      └────┘ └┘ └─┘     └┘  └┘  └───┘  └──┘   └─┘  └┘  └┘
pid            └┘ └─┘     └┘  └┘  └───┘  └──┘   └─┘  └┘  
st   ────────────────────────────────────────────────────────┘└─
143  end
st   ──┘
144  
145  theorem cof_le_card (o) : cof o ≤ card o :=
id                             └─┘   └──┘ 
src                            └─┘    └──┘
typ                            └─┘   └──┘ 
doc                            └─┘     └──┘
146  induction_on o $ λ α r _, begin
id   └──────────┘        
src  └──────────┘
typ  └──────────┘        
st                             └─────
147    resetI,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ──────────
148    have : mk (@set.univ α) = card (type r) :=
id            └┘   └──────┘    └──┘  └──┘ 
src    └─────┘└┘  └──────┘ └┘└──┘ └──┘ └────
typ    └─────┘└┘  └──────┘└┘└──┘ └──┘└────
doc    └─────┘└┘           └┘ └──┘ └──┘ └────
txt    └─────┘             └┘           └────
par    └─────┘             └┘           └────
pid    └───┘└┘             └┘           └───
st   ─────────────────────────────────────────────
149      quotient.sound ⟨equiv.set.univ _⟩,
id       └────────────┘  └────────────┘
src  ───┘└────────────┘ └────────────┘└─┘
typ  ───┘└────────────┘ └────────────┘└─┘
doc  ───┘                             └─┘
txt  ───┘                             └─┘
par  ───┘                             └─┘
pid  ───┘                             └─┘
st   ────────────────────────────────────┘└─
150    rw ← this, exact cof_type_le set.univ (λ a, ⟨a, ⟨⟩, irrefl a⟩)
id          └──┘        └─────────┘ └──────┘              └────┘
src    └───┘      └────┘└─────────┘└──────┘  └──┘  └┘└─┘└────┘ └─┘
typ    └───┘└──┘  └────┘└─────────┘└──────┘  └──┘  └┘└─┘└────┘ └─┘
doc    └───┘      └────┘                     └──┘  └┘ └─┘       └─┘
txt    └───┘      └────┘                     └──┘  └┘ └─┘       └─┘
par    └───┘      └────┘                     └──┘  └┘ └─┘       └─┘
pid      └─┘                                └──┘  └┘ └─┘       └┘
st   ──────────┘└────────────────────────────────────────────────────┘
151  end
st   └─┘
152  
153  theorem cof_ord_le (c : cardinal) : cof c.ord ≤ c :=
id                           └──────┘    └─┘ └──┘  
src                          └──────┘    └─┘  └──┘ 
typ                          └──────┘    └─┘ └──┘  
doc                          └──────┘    └─┘  └──┘
154  by simpa using cof_le_card c.ord
id                  └─────────┘ └───┘
src     └──────────┘└─────────┘└───┘
typ     └──────────┘└─────────┘└───┘
doc     └──────────┘           └───┘
txt     └──────────┘                
par     └──────────┘                
pid          └────┘                
st     └──────────────────────────────
155  
src  
typ  
doc  
txt  
par  
pid  
st   
156  @[simp] theorem cof_zero : cof 0 = 0 :=
id                              └─┘   
src                             └─┘   
typ                             └─┘   
doc    └──┘                     └─┘
157  le_antisymm (by simpa using cof_le_card 0) (cardinal.zero_le _)
id   └─────────┘                 └─────────┘     └──────────────┘
src  └─────────┘     └──────────┘└─────────┘└┘   └──────────────┘
typ  └─────────┘     └──────────┘└─────────┘└┘   └──────────────┘
doc                  └──────────┘           └┘
txt                  └──────────┘           └┘
par                  └──────────┘           └┘
pid                       └────┘           
st                  └────────────────────────┘
158  
159  @[simp] theorem cof_eq_zero {o} : cof o = 0 ↔ o = 0 :=
id                                     └─┘       
src                                    └─┘         
typ                                    └─┘       
doc    └──┘                            └─┘
160  ⟨induction_on o $ λ α r _ z, by exactI
id    └──────────┘         
src   └──────────┘                   └──────
typ   └──────────┘              └──────
doc                                  └──────
txt                                  └──────
par                                  └──────
pid                                        
st                                  └───────
161    let ⟨S, hl, e⟩ := cof_eq r in type_eq_zero_iff_empty.2 $
id             └┘       └────┘     └────────────────────┘
src  ─┘     └┘  └┘ └───┘└────┘ └──┘└────────────────────┘└─┘ 
typ  ─┘     └┘└┘└┘└───┘└────┘└──┘└────────────────────┘└─┘ 
doc  ─┘     └┘  └┘ └───┘       └──┘                      └─┘ 
txt  ─┘     └┘  └┘ └───┘       └──┘                      └─┘ 
par  ─┘     └┘  └┘ └───┘       └──┘                      └─┘ 
pid  ─┘     └┘  └┘ └───┘       └──┘                      └─┘ 
st   ───────────────────────────────────────────────────────────
162    λ ⟨a⟩, let ⟨b, h, _⟩ := hl a in
id        
src  ─┘ └┘ └─┘     └┘ └──────┘   └───
typ  ─┘ └┘└─┘     └┘ └──────┘   └───
doc  ─┘ └┘ └─┘     └┘ └──────┘   └───
txt  ─┘ └┘ └─┘     └┘ └──────┘   └───
par  ─┘ └┘ └─┘     └┘ └──────┘   └───
pid  ─┘ └┘ └─┘     └┘ └──────┘   └───
st   ──────────────────────────────────
163    ne_zero_iff_nonempty.2 (by exact ⟨⟨_, h⟩⟩) (e.trans z),
id     └──────────────────┘                        └────┘ 
src  ─┘└──────────────────┘└─┘   └────┘  └─┘ └┘└┘  └────┘ 
typ  ─┘└──────────────────┘└─┘   └─────┘  └─┘└──┘  └────┘
doc  ─┘                    └─┘   └────┘  └─┘ └┘└┘         
txt  ─┘                    └─┘   └────┘  └─┘ └┘└┘         
par  ─┘                    └─┘   └─────┘  └─┘ └──┘         
pid  ─┘                    └─┘   └─────┘  └─┘ └──┘         
st   ───────────────────────────┘└─────────────┘└───────────┘
164  λ e, by simp [e]⟩
id                
src          └────┘ 
typ         └────┘
doc          └────┘ 
txt          └────┘ 
par          └────┘ 
pid               
st          └───────┘
165  
166  @[simp] theorem cof_succ (o) : cof (succ o) = 1 :=
id                                  └─┘  └──┘   
src                                 └─┘  └──┘    
typ                                 └─┘  └──┘   
doc    └──┘                         └─┘  └──┘
167  begin
st   └─────
168    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
169    { refine induction_on o (λ α r _, _),
id              └──────────┘ 
src      └─────┘└──────────┘   └────────┘
typ      └─────┘└──────────┘  └────────┘
doc      └─────┘               └────────┘
txt      └─────┘               └────────┘
par      └─────┘               └────────┘
pid                           └────────┘
st   ───┘└────────────────────────────────┘└─
170      change cof (type _) ≤ _,
id              └─┘  └──┘    
src      └─────┘└─┘ └──┘└──┘└┘
typ      └─────┘└─┘ └──┘└──┘└┘
doc      └─────┘└─┘ └──┘└──┘ └┘
txt      └─────┘        └──┘ └┘
par      └─────┘        └──┘ └┘
pid                    └──┘ └┘
st   ──────────────────────────┘└─
171      rw [← (_ : mk _ = 1)], apply cof_type_le,
id                  └┘               └─────────┘
src      └────┘ └──┘└┘└─┘└──┘  └────┘└─────────┘
typ      └────┘ └──┘└┘└─┘└──┘  └────┘└─────────┘
doc      └────┘ └──┘└┘└─┘ └──┘  └────┘
txt      └────┘ └──┘  └─┘ └──┘  └────┘
par      └────┘ └──┘  └─┘ └──┘  └────┘
pid        └──┘ └──┘  └─┘ └──┘       
st   ───────────────────────┘└──────────────────┘└─
172      { refine λ a, ⟨sum.inr punit.star, set.mem_singleton _, _⟩,
id                      └─────┘ └────────┘  └───────────────┘
src        └─────┘ └──┘ └─────┘└────────┘└┘└───────────────┘└────┘
typ        └─────┘ └──┘ └─────┘└────────┘└┘└───────────────┘└────┘
doc        └─────┘ └──┘                  └┘                 └────┘
txt        └─────┘ └──┘                  └┘                 └────┘
par        └─────┘ └──┘                  └┘                 └────┘
pid               └──┘                  └┘                 └────┘
st   ─────┘└──────────────────────────────────────────────────────┘└─
173        rcases a with a|⟨⟨⟨⟩⟩⟩; simp [empty_relation] },
id                                      └────────────┘
src        └─────┘ └────────────┘  └────┘└────────────┘└┘
typ        └─────┘└────────────┘  └────┘└────────────┘└┘
doc        └─────┘ └────────────┘  └────┘              └┘
txt        └─────┘ └────────────┘  └────┘              └┘
par        └─────┘ └────────────┘  └────┘              └┘
pid               └────────────┘                    
st   ───────────────────────────────────────────────────┘└┘
174      { rw [cardinal.fintype_card, set.card_singleton], simp } },
id             └───────────────────┘  └────────────────┘
src        └──┘└───────────────────┘└┘└────────────────┘  └───┘
typ        └──┘└───────────────────┘└┘└────────────────┘  └───┘
doc        └──┘                     └┘                    └───┘
txt        └──┘                     └┘                    └───┘
par        └──┘                     └┘                    └───┘
pid          └┘                     └┘                        
st   ──────────────────────────────┘└──────────────────┘└──────┘└──┘
175    { rw [← cardinal.succ_zero, cardinal.succ_le],
id             └────────────────┘  └──────────────┘
src      └────┘└────────────────┘└┘└──────────────┘
typ      └────┘└────────────────┘└┘└──────────────┘
doc      └────┘                  └┘                
txt      └────┘                  └┘                
par      └────┘                  └┘                
pid        └──┘                  └┘                
st   ───────────────────────────┘└────────────────┘└──
176      simpa [lt_iff_le_and_ne, cardinal.zero_le] using
id              └──────────────┘  └──────────────┘
src      └─────┘└──────────────┘└┘└──────────────┘└───────
typ      └─────┘└──────────────┘└┘└──────────────┘└───────
doc      └─────┘                └┘                └───────
txt      └─────┘                └┘                └───────
par      └─────┘                └┘                └───────
pid                           └┘                └─────
st   ─────────────────────────────────────────────────────
177        λ h, succ_ne_zero o (cof_eq_zero.1 (eq.symm h)) }
id              └──────────┘   └─────────┘    └─────┘
src  ─────┘ └──┘└──────────┘  └─────────┘└─┘ └─────┘ └─┘
typ  ─────┘ └──┘└──────────┘ └─────────┘└─┘ └─────┘ └─┘
doc  ─────┘ └──┘                         └─┘         └─┘
txt  ─────┘ └──┘                         └─┘         └─┘
par  ─────┘ └──┘                         └─┘         └─┘
pid  ─────┘ └──┘                         └─┘         └┘
st   ─────────────────────────────────────────────────────┘└─
178  end
st   ──┘
179  
180  @[simp] theorem cof_eq_one_iff_is_succ {o} : cof.{u} o = 1 ↔ ∃ a, o = succ a :=
id                                                └─┘              └──┘ 
src                                               └─┘                 └──┘
typ                                               └─┘              └──┘ 
doc    └──┘                                       └─┘                      └──┘
181  ⟨induction_on o $ λ α r _ z, begin
id    └──────────┘         
src   └──────────┘
typ   └──────────┘         
st                                └─────
182    resetI,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ──────────
183    rcases cof_eq r with ⟨S, hl, e⟩, rw z at e,
id            └────┘                      
src    └─────┘└────┘ └──────────────┘  └─┘ └───┘
typ    └─────┘└────┘└──────────────┘  └─┘└───┘
doc    └─────┘       └──────────────┘  └─┘ └───┘
txt    └─────┘       └──────────────┘  └─┘ └───┘
par    └─────┘       └──────────────┘  └─┘ └───┘
pid                 └──────────────┘     └───┘
st   ────────────────────────────────┘└─────────┘└─
184    cases ne_zero_iff_nonempty.1 (by rw e; exact one_ne_zero) with a,
id           └──────────────────┘                  └─────────┘
src    └────┘└──────────────────┘└─┘   └─┘ └┘└────┘└─────────┘└──────┘
typ    └────┘└──────────────────┘└─┘   └─┘└┘└────┘└─────────┘└──────┘
doc    └────┘                    └─┘   └─┘ └┘└────┘           └──────┘
txt    └────┘                    └─┘   └─┘ └┘└────┘           └──────┘
par    └────┘                    └─┘   └─┘ └┘└────┘           └──────┘
pid                             └─┘   └──┘ └──────┘           └─────┘
st   ─────────────────────────────────┘└──────────────────────┘└──────┘└─
185    refine ⟨typein r a, eq.symm $ quotient.sound
id             └────┘    └─────┘   └────────────┘
src    └─────┘ └────┘  └┘└─────┘ └────────────┘
typ    └─────┘ └────┘└┘└─────┘ └────────────┘
doc    └─────┘ └────┘  └┘                      
txt    └─────┘         └┘                      
par    └─────┘         └┘                      
pid                   └┘                      
st   ───────────────────────────────────────────────
186      ⟨order_iso.of_surjective (order_embedding.of_monotone _
id        └─────────────────────┘  └─────────────────────────┘
src  ───┘ └─────────────────────┘ └─────────────────────────┘└──
typ  ───┘ └─────────────────────┘ └─────────────────────────┘└──
doc  ───┘                         └─────────────────────────┘└──
txt  ───┘                                                    └──
par  ───┘                                                    └──
pid  ───┘                                                    └──
st   ────────────────────────────────────────────────────────────
187        (λ x y, _)) (λ x, _)⟩⟩,
src  ─────┘  └────────┘  └──────┘
typ  ─────┘  └────────┘  └──────┘
doc  ─────┘  └────────┘  └──────┘
txt  ─────┘  └────────┘  └──────┘
par  ─────┘  └────────┘  └──────┘
pid  ─────┘  └────────┘  └──────┘
st   ───────────────────────────┘└─
188    { apply sum.rec; [exact subtype.val, exact λ _, a] },
id             └─────┘        └─────────┘             
src      └────┘└─────┘  └────┘└─────────┘  └────┘ └──┘
typ      └────┘└─────┘  └────┘└─────────┘  └────┘ └──┘
doc      └────┘          └────┘             └────┘ └──┘
txt      └────┘          └────┘             └────┘ └──┘
par      └────┘          └────┘             └────┘ └──┘
pid                                             └──┘
st   ───┘└──────────────────────────────────────────────┘└─┘
189    { rcases x with x|⟨⟨⟨⟩⟩⟩; rcases y with y|⟨⟨⟨⟩⟩⟩;
id                                     
src      └─────┘ └────────────┘  └─────┘ └────────────┘
typ      └─────┘└────────────┘  └─────┘└────────────┘
doc      └─────┘ └────────────┘  └─────┘ └────────────┘
txt      └─────┘ └────────────┘  └─────┘ └────────────┘
par      └─────┘ └────────────┘  └─────┘ └────────────┘
pid             └────────────┘         └────────────┘
st   ───┘└───────────────────────────────────────────────
190        simp [subrel, order.preimage, empty_relation],
id               └────┘  └────────────┘  └────────────┘
src        └────┘└────┘└┘└────────────┘└┘└────────────┘
typ        └────┘└────┘└┘└────────────┘└┘└────────────┘
doc        └────┘└────┘└┘└────────────┘└┘              
txt        └────┘      └┘              └┘              
par        └────┘      └┘              └┘              
pid                  └┘              └┘              
st   ──────────────────────────────────────────────────┘└─
191      exact x.2 },
id             
src      └────┘ └─┘
typ      └────┘└─┘
doc      └────┘ └─┘
txt      └────┘ └─┘
par      └────┘ └─┘
pid            └─┘
st   ─────────────┘└┘
192    { suffices : r x a ∨ ∃ (b : punit), ↑a = x, {simpa},
id                               └───┘    
src      └─────────┘    └────┘└───┘     └───┘
typ      └─────────┘   └────┘└───┘   └───┘
doc      └─────────┘     └────┘             └───┘
txt      └─────────┘     └────┘             └───┘
par      └─────────┘     └────┘             └───┘
pid      └───────┘└┘     └────┘         
st   ───────────────────────────────────────────┘└──────┘└┘
193      rcases trichotomous_of r x a with h|h|h,
id              └─────────────┘   
src      └─────┘└─────────────┘   └─────────┘
typ      └─────┘└─────────────┘└─────────┘
doc      └─────┘                  └─────────┘
txt      └─────┘                  └─────────┘
par      └─────┘                  └─────────┘
pid                              └─────────┘
st   ──────────────────────────────────────────┘└─
194      { exact or.inl h },
id               └────┘ 
src        └────┘└────┘ 
typ        └────┘└────┘
doc        └────┘       
txt        └────┘       
par        └────┘       
pid                    
st   ─────┘└─────────────┘└┘
195      { exact or.inr ⟨punit.star, h.symm⟩ },
id               └────┘  └────────┘  └────┘
src        └────┘└────┘ └────────┘└┘└────┘└┘
typ        └────┘└────┘ └────────┘└┘└────┘└┘
doc        └────┘                 └┘      └┘
txt        └────┘                 └┘      └┘
par        └────┘                 └┘      └┘
pid                              └┘      
st   ─────┘└────────────────────────────────┘└┘
196      { rcases hl x with ⟨a', aS, hn⟩,
id                └┘ 
src        └─────┘   └────────────────┘
typ        └─────┘└┘└────────────────┘
doc        └─────┘   └────────────────┘
txt        └─────┘   └────────────────┘
par        └─────┘   └────────────────┘
pid                 └────────────────┘
st   ──────────────────────────────────┘└─
197        rw (_ : ↑a = a') at h, {exact absurd h hn},
id                     └┘               └────┘  └┘
src        └─┘ └──┘     └────┘   └────┘└────┘ 
typ        └─┘ └──┘  └┘└────┘   └────┘└────┘└┘
doc        └─┘ └──┘     └────┘   └────┘       
txt        └─┘ └──┘     └────┘   └────┘       
par        └─┘ └──┘     └────┘   └────┘       
pid           └──┘     └───┘               
st   ──────────────────────────┘└──────────────────┘└┘
198        refine congr_arg subtype.val (_ : a = ⟨a', aS⟩),
id                └───────┘ └─────────┘          └┘  └┘
src        └─────┘└───────┘└─────────┘ └──┘     └┘  └┘
typ        └─────┘└───────┘└─────────┘ └──┘  └┘└┘└┘└┘
doc        └─────┘                     └──┘     └┘  └┘
txt        └─────┘                     └──┘     └┘  └┘
par        └─────┘                     └──┘     └┘  └┘
pid                                   └──┘     └┘  └┘
st   ────────────────────────────────────────────────────┘└─
199        haveI := le_one_iff_subsingleton.1 (le_of_eq e),
id                  └─────────────────────┘    └──────┘ 
src        └───────┘└─────────────────────┘└─┘ └──────┘ 
typ        └───────┘└─────────────────────┘└─┘ └──────┘
doc        └───────┘                       └─┘          
txt        └───────┘                       └─┘          
par        └───────┘                       └─┘          
pid             └─┘                       └─┘          
st   ────────────────────────────────────────────────────┘└─
200        apply subsingleton.elim } }
id               └───────────────┘
src        └────┘└───────────────┘
typ        └────┘└───────────────┘
doc        └────┘                 
txt        └────┘                 
par        └────┘                 
pid                              
st   ─────────────────────────────┘└───
201  end, λ ⟨a, e⟩, by simp [e]⟩
id                          
src                    └────┘ 
typ                   └────┘
doc                    └────┘ 
txt                    └────┘ 
par                    └────┘ 
pid                         
st   ──┘              └───────┘
202  
203  @[simp] theorem cof_add (a b : ordinal) : b ≠ 0 → cof (a + b) = cof b :=
id                                  └─────┘          └─┘       └─┘ 
src                                 └─────┘           └─┘         └─┘
typ                                 └─────┘          └─┘       └─┘ 
doc    └──┘                         └─────┘            └─┘           └─┘
204  induction_on a $ λ α r _, induction_on b $ λ β s _ b0, begin
id   └──────────┘          └──────────┘         └┘
src  └──────────┘              └──────────┘
typ  └──────────┘          └──────────┘         └┘
st                                                          └─────
205    resetI,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ──────────
206    change cof (type _) = _,
id            └─┘  └──┘    
src    └─────┘└─┘ └──┘└──┘└┘
typ    └─────┘└─┘ └──┘└──┘└┘
doc    └─────┘└─┘ └──┘└──┘ └┘
txt    └─────┘        └──┘ └┘
par    └─────┘        └──┘ └┘
pid                  └──┘ └┘
st   ────────────────────────┘└─
207    refine eq_of_forall_le_iff (λ c, _),
id            └─────────────────┘
src    └─────┘└─────────────────┘  └────┘
typ    └─────┘└─────────────────┘  └────┘
doc    └─────┘                     └────┘
txt    └─────┘                     └────┘
par    └─────┘                     └────┘
pid                               └────┘
st   ────────────────────────────────────┘└─
208    rw [le_cof_type, le_cof_type],
id         └─────────┘  └─────────┘
src    └──┘└─────────┘└┘└─────────┘
typ    └──┘└─────────┘└┘└─────────┘
doc    └──┘           └┘           
txt    └──┘           └┘           
par    └──┘           └┘           
pid      └┘           └┘           
st   ────────────────┘└───────────┘└──
209    split; intros H S hS,
src    └───┘  └───────────┘
typ    └───┘  └───────────┘
doc    └───┘  └───────────┘
txt    └───┘  └───────────┘
par    └───┘  └───────────┘
pid                 └─────┘
st   ─────────────────────┘└─
210    { refine le_trans (H {a | sum.rec_on a (∅:set α) S} (λ a, _)) ⟨⟨_, _⟩⟩,
id              └──────┘       └────────┘     └─┘   
src      └─────┘└──────┘  └──┘└────────┘  └─┘ └┘ └┘  └──────┘  └────┘
typ      └─────┘└──────┘ └──┘└────────┘  └─┘└┘└┘  └──────┘  └────┘
doc      └─────┘           └──┘                 └┘ └┘  └──────┘  └────┘
txt      └─────┘           └──┘                 └┘ └┘  └──────┘  └────┘
par      └─────┘           └──┘                 └┘ └┘  └──────┘  └────┘
pid                       └──┘                 └┘ └┘  └──────┘  └────┘
st   ───┘└──────────────────────────────────────────────────────────────────┘└─
211      { cases a with a b,
id               
src        └────┘ └───────┘
typ        └────┘└───────┘
doc        └────┘ └───────┘
txt        └────┘ └───────┘
par        └────┘ └───────┘
pid              └───────┘
st   ─────┘└──────────────┘└─
212        { cases type_ne_zero_iff_nonempty.1 b0 with b,
id                 └───────────────────────┘   └┘
src          └────┘└───────────────────────┘└─┘  └─────┘
typ          └────┘└───────────────────────┘└─┘└┘└─────┘
doc          └────┘                         └─┘  └─────┘
txt          └────┘                         └─┘  └─────┘
par          └────┘                         └─┘  └─────┘
pid                                        └─┘  └─────┘
st   ───────┘└─────────────────────────────────────────┘└─
213          rcases hS b with ⟨b', bs, _⟩,
id                  └┘ 
src          └─────┘   └───────────────┘
typ          └─────┘└┘└───────────────┘
doc          └─────┘   └───────────────┘
txt          └─────┘   └───────────────┘
par          └─────┘   └───────────────┘
pid                   └───────────────┘
st   ───────────────────────────────────┘└─
214          exact ⟨sum.inr b', bs, by simp⟩ },
id                  └─────┘ └┘  └┘
src          └────┘ └─────┘  └┘  └┘  └──┘└┘
typ          └────┘ └─────┘└┘└┘└┘└┘  └──┘└┘
doc          └────┘          └┘  └┘  └──┘└┘
txt          └────┘          └┘  └┘  └──┘└┘
par          └────┘          └┘  └┘  └──┘└┘
pid                         └┘  └┘  └────┘
st   ────────────────────────────────┘└───┘└┘└┘
215        { rcases hS b with ⟨b', bs, h⟩,
id                  └┘ 
src          └─────┘   └───────────────┘
typ          └─────┘└┘└───────────────┘
doc          └─────┘   └───────────────┘
txt          └─────┘   └───────────────┘
par          └─────┘   └───────────────┘
pid                   └───────────────┘
st   ───────────────────────────────────┘└─
216          exact ⟨sum.inr b', bs, by simp [h]⟩ } },
id                  └─────┘ └┘  └┘           
src          └────┘ └─────┘  └┘  └┘  └────┘ └┘
typ          └────┘ └─────┘└┘└┘└┘└┘  └────┘└┘
doc          └────┘          └┘  └┘  └────┘ └┘
txt          └────┘          └┘  └┘  └────┘ └┘
par          └────┘          └┘  └┘  └────┘ └┘
pid                         └┘  └┘  └─────┘ └┘
st   ────────────────────────────────┘└───────┘└┘└──┘
217      { exact λ a, match a with ⟨sum.inr b, h⟩ := ⟨b, h⟩ end },
id                                            
src        └────┘ └──┘      └────┘         └┘ └───┘  └┘ └────┘
typ        └────┘ └──┘      └────┘        └┘└───┘  └┘ └────┘
doc        └────┘ └──┘      └────┘         └┘ └───┘  └┘ └────┘
txt        └────┘ └──┘      └────┘         └┘ └───┘  └┘ └────┘
par        └────┘ └──┘      └────┘         └┘ └───┘  └┘ └────┘
pid              └──┘      └────┘         └┘ └───┘  └┘ └───┘
st   ─────┘└───────────────────────────────────────────────────┘└┘
218      { exact λ a b, match a, b with
src        └────┘ └────┘      └┘ └─────
typ        └────┘ └────┘      └┘ └─────
doc        └────┘ └────┘      └┘ └─────
txt        └────┘ └────┘      └┘ └─────
par        └────┘ └────┘      └┘ └─────
pid              └────┘      └┘ └─────
st   ───────────────────────────────────
219          ⟨sum.inr a, h₁⟩, ⟨sum.inr b, h₂⟩, h := by congr; injection h
id                                                                      
src  ───────┘         └┘  └─┘         └┘  └─┘ └──┘  └───┘└┘└────────┘ 
typ  ───────┘         └┘  └─┘         └┘  └─┘ └──┘  └───┘└┘└────────┘
doc  ───────┘         └┘  └─┘         └┘  └─┘ └──┘       └┘└────────┘ 
txt  ───────┘         └┘  └─┘         └┘  └─┘ └──┘  └───┘└┘└────────┘ 
par  ───────┘         └┘  └─┘         └┘  └─┘ └──┘  └───┘└┘└────────┘ 
pid  ───────┘         └┘  └─┘         └┘  └─┘ └──┘  └────────────────┘ 
st   ────────────────────────────────────────────────┘└───────────────────
220        end } },
src  ─────┘└──┘
typ  ─────┘└──┘
doc  ─────┘└──┘
txt  ─────┘└──┘
par  ─────┘└──┘
pid  ────────┘
st   ─────┘└──┘└──┘
221    { refine le_trans (H (sum.inr ⁻¹' S) (λ a, _)) ⟨⟨_, _⟩⟩,
id              └──────┘    └─────┘ └─┘ 
src      └─────┘└──────┘   └─────┘└─┘ └┘  └──────┘  └────┘
typ      └─────┘└──────┘  └─────┘└─┘└┘  └──────┘  └────┘
doc      └─────┘                  └─┘ └┘  └──────┘  └────┘
txt      └─────┘                      └┘  └──────┘  └────┘
par      └─────┘                      └┘  └──────┘  └────┘
pid                                  └┘  └──────┘  └────┘
st   ────────────────────────────────────────────────────────┘└─
222      { rcases hS (sum.inr a) with ⟨a'|b', bs, h⟩; simp at h,
id                └┘  └─────┘ 
src        └─────┘   └─────┘ └───────────────────┘  └───────┘
typ        └─────┘└┘ └─────┘└───────────────────┘  └───────┘
doc        └─────┘           └───────────────────┘  └───────┘
txt        └─────┘           └───────────────────┘  └───────┘
par        └─────┘           └───────────────────┘  └───────┘
pid                         └───────────────────┘      └──┘
st   ─────┘└──────────────────────────────────────────────────┘└─
223        { cases h }, { exact ⟨b', bs, h⟩ } },
id                              └┘  └┘  
src          └────┘      └────┘   └┘  └┘ └┘
typ          └────┘     └────┘ └┘└┘└┘└┘└┘
doc          └────┘      └────┘   └┘  └┘ └┘
txt          └────┘      └────┘   └┘  └┘ └┘
par          └────┘      └────┘   └┘  └┘ └┘
pid                             └┘  └┘ 
st   ───────┘└──────┘└┘└───────────────────┘└──┘
224      { exact λ ⟨a, h⟩, ⟨_, h⟩ },
id                     
src        └────┘ └┘ └┘ └─┘ └─┘ └┘
typ        └────┘ └┘ └┘└─┘ └─┘ └┘
doc        └────┘ └┘ └┘ └─┘ └─┘ └┘
txt        └────┘ └┘ └┘ └─┘ └─┘ └┘
par        └────┘ └┘ └┘ └─┘ └─┘ └┘
pid              └┘ └┘ └─┘ └─┘ 
st   ─────┘└─────────────────────┘└┘
225      { exact λ ⟨a, h₁⟩ ⟨b, h₂⟩ h,
src        └────┘ └┘ └┘  └─┘ └┘  └────
typ        └────┘ └┘ └┘  └─┘ └┘  └────
doc        └────┘ └┘ └┘  └─┘ └┘  └────
txt        └────┘ └┘ └┘  └─┘ └┘  └────
par        └────┘ └┘ └┘  └─┘ └┘  └────
pid              └┘ └┘  └─┘ └┘  └────
st   ─────────────────────────────────
226          by injection h with h; congr; injection h } }
id                                                  
src  ───────┘  └────────┘ └─────┘└┘└───┘└┘└────────┘ 
typ  ───────┘  └────────┘└─────┘└┘└───┘└┘└────────┘
doc  ───────┘  └────────┘ └─────┘└┘     └┘└────────┘ 
txt  ───────┘  └────────┘ └─────┘└┘└───┘└┘└────────┘ 
par  ───────┘  └────────┘ └─────┘└┘└───┘└┘└────────┘ 
pid  ───────┘  └─────────┘ └────────────────────────┘ 
st   ─────────┘└──────────────────────────────────────┘└───
227  end
st   ──┘
228  
229  @[simp] theorem cof_cof (o : ordinal) : cof (cof o).ord = cof o :=
id                                └─────┘    └─┘  └─┘  └─┘   └─┘ 
src                               └─────┘    └─┘  └─┘   └─┘   └─┘
typ                               └─────┘    └─┘  └─┘  └─┘   └─┘ 
doc    └──┘                       └─────┘    └─┘  └─┘   └─┘    └─┘
230  le_antisymm (le_trans (cof_le_card _) (by simp)) $
id   └─────────┘  └──────┘  └─────────┘
src  └─────────┘  └──────┘  └─────────┘        └──┘
typ  └─────────┘  └──────┘  └─────────┘        └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
231  induction_on o $ λ α r _, by exactI
id   └──────────┘        
src  └──────────┘                 └─────┘
typ  └──────────┘             └─────┘
doc                               └─────┘
txt                               └─────┘
par                               └─────┘
pid                                     
st                               └───────
232  let ⟨S, hS, e₁⟩ := ord_cof_eq r,
id                     └────────┘ 
src       └┘  └┘  └───┘└────────┘ └─
typ      └┘  └┘  └───┘└────────┘└─
doc       └┘  └┘  └───┘           └─
txt       └┘  └┘  └───┘           └─
par       └┘  └┘  └───┘           └─
pid       └┘  └┘  └───┘           └─
st   ─────────────────────────────────
233      ⟨T, hT, e₂⟩ := cof_eq (subrel r S) in begin
id                      └────┘  └────┘
src  ───┘  └┘  └┘  └───┘└────┘ └────┘  └───┘     
typ  ───┘  └┘  └┘  └───┘└────┘ └────┘  └───┘     
doc  ───┘  └┘  └┘  └───┘       └────┘  └───┘     
txt  ───┘  └┘  └┘  └───┘               └───┘     
par  ───┘  └┘  └┘  └───┘               └───┘     
pid  ───┘  └┘  └┘  └───┘               └───┘     
st   ─────────────────────────────────────────┘└─────
234    rw e₁ at e₂, rw ← e₂,
id        └┘             └┘
src  ─┘└─┘  └────┘└┘└───┘  └─
typ  ─┘└─┘└┘└────┘└┘└───┘└┘└─
doc  ─┘└─┘  └────┘└┘└───┘  └─
txt  ─┘└─┘  └────┘└┘└───┘  └─
par  ─┘└─┘  └────┘└┘└───┘  └─
pid  ────┘  └───────────┘  └─
st   ────────────┘└───────┘└─
235    refine le_trans (cof_type_le {a | ∃ h, (subtype.mk a h : S) ∈ T} (λ a, _)) ⟨⟨_, _⟩⟩,
id            └──────┘  └─────────┘         └────────┘          
src  ─┘└─────┘└──────┘ └─────────┘└──┘└┘ └────────┘  └─┘ └┘ └┘  └──────┘  └────┘└─
typ  ────────┘└──────┘ └─────────┘└──┘└┘ └────────┘  └─┘└┘└┘  └──────┘  └───────
doc  ─┘└─────┘                     └──┘ └┘              └─┘ └┘  └┘  └──────┘  └────┘└─
txt  ─┘└─────┘                     └──┘ └┘              └─┘ └┘  └┘  └──────┘  └────┘└─
par  ────────┘                     └──┘ └┘              └─┘ └┘  └┘  └──────┘  └───────
pid  ────────┘                     └──┘ └┘              └─┘ └┘  └┘  └──────┘  └───────
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
236    { rcases hS a with ⟨b, bS, br⟩,
id              └┘ 
src  ───┘└─────┘   └───────────────┘└─
typ  ───┘└─────┘└┘└───────────────┘└─
doc  ───┘└─────┘   └───────────────┘└─
txt  ───┘└─────┘   └───────────────┘└─
par  ───┘└─────┘   └───────────────┘└─
pid  ──────────┘   └──────────────────
st   ──┘└───────────────────────────┘└─
237      rcases hT ⟨b, bS⟩ with ⟨⟨c, cS⟩, cT, cs⟩,
id              └┘    └┘
src  ───┘└─────┘    └┘  └──────────────────────┘└─
typ  ───┘└─────┘└┘ └┘└┘└──────────────────────┘└─
doc  ───┘└─────┘    └┘  └──────────────────────┘└─
txt  ───┘└─────┘    └┘  └──────────────────────┘└─
par  ───┘└─────┘    └┘  └──────────────────────┘└─
pid  ──────────┘    └┘  └─────────────────────────
st   ───────────────────────────────────────────┘└─
238      exact ⟨c, ⟨cS, cT⟩, is_order_connected.neg_trans cs br⟩ },
id                 └┘  └┘   └──────────────────────────┘ └┘ └┘
src  ───┘└────┘  └┘   └┘  └─┘└──────────────────────────┘    └┘└──
typ  ─────────┘ └┘ └┘└┘└┘└─┘└──────────────────────────┘└┘└┘└────
doc  ───┘└────┘  └┘   └┘  └─┘                                └┘└──
txt  ───┘└────┘  └┘   └┘  └─┘                                └┘└──
par  ─────────┘  └┘   └┘  └─┘                                └────
pid  ─────────┘  └┘   └┘  └─┘                                └────
st   ───────────────────────────────────────────────────────────┘└─
239    { exact λ ⟨a, h⟩, ⟨⟨a, h.fst⟩, h.snd⟩ },
id                           └──┘    └──┘
src  ───┘└────┘ └┘ └┘ └─┘   └┘ └──┘└─┘ └──┘└┘└──
typ  ─────────┘ └┘└┘└─┘   └┘ └──┘└─┘ └──┘└────
doc  ───┘└────┘ └┘ └┘ └─┘   └┘     └─┘     └┘└──
txt  ───┘└────┘ └┘ └┘ └─┘   └┘     └─┘     └┘└──
par  ─────────┘ └┘ └┘ └─┘   └┘     └─┘     └────
pid  ─────────┘ └┘ └┘ └─┘   └┘     └─┘     └────
st   ──┘└───────────────────────────────────┘└─
240    { exact λ ⟨a, ha⟩ ⟨b, hb⟩ h,
src  ───┘└────┘ └┘ └┘  └─┘ └┘  └────
typ  ─────────┘ └┘ └┘  └─┘ └┘  └────
doc  ───┘└────┘ └┘ └┘  └─┘ └┘  └────
txt  ───┘└────┘ └┘ └┘  └─┘ └┘  └────
par  ─────────┘ └┘ └┘  └─┘ └┘  └────
pid  ─────────┘ └┘ └┘  └─┘ └┘  └────
st   ───────────────────────────────
241        by injection h with h; congr; injection h },
id                                                
src  ─────┘  └────────┘ └─────┘└┘└───┘└┘└────────┘ └──
typ  ─────┘  └────────┘└─────┘└┘└───┘└┘└────────┘└──
doc  ─────┘  └────────┘ └─────┘└┘     └┘└────────┘ └──
txt  ─────┘  └────────┘ └─────┘└┘└───┘└┘└────────┘ └──
par  ─────┘  └────────┘ └─────┘└┘└───┘└┘└────────┘ └──
pid  ─────┘  └─────────┘ └────────────────────────┘ └───
st   ───────┘└──────────────────────────────────────┘└──
242  end
src  ────
typ  ────
doc  ────
txt  ────
par  ────
pid  ──┘
st   ──┘
243  
src  
typ  
doc  
txt  
par  
pid  
st   
244  theorem omega_le_cof {o} : cardinal.omega ≤ cof o ↔ is_limit o :=
id                              └────────────┘  └─┘   └──────┘ 
src                             └────────────┘  └─┘    └──────┘
typ                             └────────────┘  └─┘   └──────┘ 
doc                             └────────────┘   └─┘     └──────┘
245  begin
st   └─────
246    rcases zero_or_succ_or_limit o with rfl|⟨o,rfl⟩|l,
id            └───────────────────┘ 
src    └─────┘└───────────────────┘ └─────────────────┘
typ    └─────┘└───────────────────┘└─────────────────┘
doc    └─────┘                      └─────────────────┘
txt    └─────┘                      └─────────────────┘
par    └─────┘                      └─────────────────┘
pid                                └─────────────────┘
st   ──────────────────────────────────────────────────┘└─
247    { simp [not_zero_is_limit, cardinal.omega_ne_zero] },
id             └───────────────┘  └────────────────────┘
src      └────┘└───────────────┘└┘└────────────────────┘└┘
typ      └────┘└───────────────┘└┘└────────────────────┘└┘
doc      └────┘                 └┘                      └┘
txt      └────┘                 └┘                      └┘
par      └────┘                 └┘                      └┘
pid                           └┘                      
st   ───┘└───────────────────────────────────────────────┘└┘
248    { simp [not_succ_is_limit, cardinal.one_lt_omega] },
id             └───────────────┘  └───────────────────┘
src      └────┘└───────────────┘└┘└───────────────────┘└┘
typ      └────┘└───────────────┘└┘└───────────────────┘└┘
doc      └────┘                 └┘                     └┘
txt      └────┘                 └┘                     └┘
par      └────┘                 └┘                     └┘
pid                           └┘                     
st   ───┘└──────────────────────────────────────────────┘└┘
249    { simp [l], refine le_of_not_lt (λ h, _),
id                       └──────────┘
src      └────┘   └─────┘└──────────┘  └────┘
typ      └────┘  └─────┘└──────────┘  └────┘
doc      └────┘   └─────┘              └────┘
txt      └────┘   └─────┘              └────┘
par      └────┘   └─────┘              └────┘
pid                                 └────┘
st   ───────────┘└────────────────────────────┘└─
250      cases cardinal.lt_omega.1 h with n e,
id             └───────────────┘   
src      └────┘└───────────────┘└─┘ └───────┘
typ      └────┘└───────────────┘└─┘└───────┘
doc      └────┘                 └─┘ └───────┘
txt      └────┘                 └─┘ └───────┘
par      └────┘                 └─┘ └───────┘
pid                            └─┘ └───────┘
st   ───────────────────────────────────────┘└─
251      have := cof_cof o,
id               └─────┘ 
src      └──────┘└─────┘
typ      └──────┘└─────┘
doc      └──────┘       
txt      └──────┘       
par      └──────┘       
pid      └───┘└─┘       
st   ────────────────────┘└─
252      rw [e, ord_nat] at this,
id             └─────┘
src      └──┘ └┘└─────┘└───────┘
typ      └──┘└┘└─────┘└───────┘
doc      └──┘ └┘       └───────┘
txt      └──┘ └┘       └───────┘
par      └──┘ └┘       └───────┘
pid        └┘ └┘       └──────┘
st   ────────┘└───────┘└──────┘└─
253      cases n,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
254      { simp at e, simpa [e, not_zero_is_limit] using l },
id                             └───────────────┘        
src        └───────┘  └─────┘ └┘└───────────────┘└──────┘ 
typ        └───────┘  └─────┘└┘└───────────────┘└──────┘
doc        └───────┘  └─────┘ └┘                 └──────┘ 
txt        └───────┘  └─────┘ └┘                 └──────┘ 
par        └───────┘  └─────┘ └┘                 └──────┘ 
pid            └──┘        └┘                 └────┘ 
st   ─────┘└───────┘└─────────────────────────────────────┘└┘
255      { rw [← nat_cast_succ, cof_succ] at this,
id               └───────────┘  └──────┘
src        └────┘└───────────┘└┘└──────┘└───────┘
typ        └────┘└───────────┘└┘└──────┘└───────┘
doc        └────┘             └┘        └───────┘
txt        └────┘             └┘        └───────┘
par        └────┘             └┘        └───────┘
pid          └──┘             └┘        └──────┘
st   ────────────────────────┘└────────┘└──────┘└─
256        rw [← this, cof_eq_one_iff_is_succ] at e,
id               └──┘  └────────────────────┘
src        └────┘    └┘└────────────────────┘└────┘
typ        └────┘└──┘└┘└────────────────────┘└────┘
doc        └────┘    └┘                      └────┘
txt        └────┘    └┘                      └────┘
par        └────┘    └┘                      └────┘
pid          └──┘    └┘                      └───┘
st   ───────────────┘└──────────────────────┘└───┘└─
257        rcases e with ⟨a, rfl⟩,
id                
src        └─────┘ └────────────┘
typ        └─────┘└────────────┘
doc        └─────┘ └────────────┘
txt        └─────┘ └────────────┘
par        └─────┘ └────────────┘
pid               └────────────┘
st   ───────────────────────────┘└─
258        exact not_succ_is_limit _ l } }
id               └───────────────┘   
src        └────┘└───────────────┘└─┘ 
typ        └────┘└───────────────┘└─┘
doc        └────┘                 └─┘ 
txt        └────┘                 └─┘ 
par        └────┘                 └─┘ 
pid                              └─┘ 
st   ─────────────────────────────────┘└───
259  end
st   ──┘
260  
261  @[simp] theorem cof_omega : cof omega = cardinal.omega :=
id                               └─┘ └───┘  └────────────┘
src                              └─┘ └───┘  └────────────┘
typ                              └─┘ └───┘  └────────────┘
doc    └──┘                      └─┘ └───┘   └────────────┘
262  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
263    (by rw ← card_omega; apply cof_le_card)
id              └────────┘        └─────────┘
src        └───┘└────────┘  └────┘└─────────┘
typ        └───┘└────────┘  └────┘└─────────┘
doc        └───┘            └────┘
txt        └───┘            └────┘
par        └───┘            └────┘
pid          └─┘                 
st        └─────────────────────────────────┘
264    (omega_le_cof.2 omega_is_limit)
id      └──────────┘  └────────────┘
src     └──────────┘  └────────────┘
typ     └──────────┘  └────────────┘
265  
266  theorem cof_eq' (r : α → α → Prop) [is_well_order α r] (h : is_limit (type r)) :
id                                     └───────────┘         └──────┘  └──┘ 
src                                      └───────────┘           └──────┘  └──┘
typ                                    └───────────┘         └──────┘  └──┘ 
doc                                      └───────────┘           └──────┘  └──┘
267    ∃ S : set α, (∀ a, ∃ b ∈ S, r a b) ∧ mk S = cof (type r) :=
id          └─┘                 └┘   └─┘  └──┘ 
src         └─┘                        └┘    └─┘  └──┘
typ         └─┘                 └┘   └─┘  └──┘ 
doc                                         └┘     └─┘  └──┘
268  let ⟨S, H, e⟩ := cof_eq r in
id   └─┘           └────┘ 
src                   └────┘
typ  └─┘           └────┘ 
269  ⟨S, λ a,
id         
typ        
270    let a' := enum r _ (h.2 _ (typein_lt_type r a)) in
id         └┘    └──┘          └────────────┘  
src              └──┘            └────────────┘
typ        └┘    └──┘          └────────────┘  
doc              └──┘
271    let ⟨b, h, ab⟩ := H a' in
id     └─┘      └┘       └┘
typ    └─┘      └┘       └┘
272    ⟨b, h, (is_order_connected.conn a b a' $ (typein_lt_typein r).1
id             └─────────────────────┘    └┘    └──────────────┘  
src            └─────────────────────┘           └──────────────┘   
typ            └─────────────────────┘    └┘    └──────────────┘  
273      (by rw typein_enum; apply ordinal.lt_succ_self)).resolve_right ab⟩,
id              └─────────┘        └──────────────────┘  └───────────┘
src          └─┘└─────────┘  └────┘└──────────────────┘  └───────────┘
typ          └─┘└─────────┘  └────┘└──────────────────┘  └───────────┘
doc          └─┘             └────┘
txt          └─┘             └────┘
par          └─┘             └────┘
pid                              
st          └─────────────────────────────────────────┘
274  e⟩
275  
276  theorem cof_sup_le_lift {ι} (f : ι → ordinal) (H : ∀ i, f i < sup f) :
id                                       └─────┘              └─┘ 
src                                       └─────┘                 └─┘
typ                                      └─────┘              └─┘ 
doc                                       └─────┘                  └─┘
277    cof (sup f) ≤ (mk ι).lift :=
id     └─┘  └─┘     └┘  └──┘
src    └─┘  └─┘      └┘   └──┘
typ    └─┘  └─┘     └┘  └──┘
doc    └─┘  └─┘       └┘   └──┘
278  begin
st   └─────
279    generalize e : sup f = o,
id                    └─┘ 
src    └─────────────┘└─┘  
typ    └─────────────┘└─┘ 
doc    └─────────────┘└─┘  
txt    └─────────────┘     
par    └─────────────┘     
pid              └┘└┘     
st   ─────────────────────────┘└─
280    refine ordinal.induction_on o _ e, introsI α r _ e',
id            └──────────────────┘    
src    └─────┘└──────────────────┘ └─┘   └──────────────┘
typ    └─────┘└──────────────────┘└─┘  └──────────────┘
doc    └─────┘                     └─┘   └──────────────┘
txt    └─────┘                     └─┘   └──────────────┘
par    └─────┘                     └─┘   └──────────────┘
pid                               └─┘          └───────┘
st   ──────────────────────────────────┘└────────────────┘└─
281    rw e' at H,
id        └┘
src    └─┘  └───┘
typ    └─┘└┘└───┘
doc    └─┘  └───┘
txt    └─┘  └───┘
par    └─┘  └───┘
pid        └───┘
st   ───────────┘└─
282    refine le_trans (cof_type_le (set.range (λ i, enum r _ (H i))) _)
id            └──────┘  └─────────┘  └───────┘       └──┘     
src    └─────┘└──────┘ └─────────┘ └───────┘  └──┘└──┘ └─┘   └──────
typ    └─────┘└──────┘ └─────────┘ └───────┘  └──┘└──┘└─┘  └──────
doc    └─────┘                     └───────┘  └──┘└──┘ └─┘   └──────
txt    └─────┘                                └──┘     └─┘   └──────
par    └─────┘                                └──┘     └─┘   └──────
pid                                          └──┘     └─┘   └──────
st   ────────────────────────────────────────────────────────────────────
283      ⟨embedding.of_surjective _⟩,
id        └─────────────────────┘
src  ───┘ └─────────────────────┘└─┘
typ  ───┘ └─────────────────────┘└─┘
doc  ───┘                        └─┘
txt  ───┘                        └─┘
par  ───┘                        └─┘
pid  ───┘                        └─┘
st   ──────────────────────────────┘└─
284    { intro a, by_contra h,
src      └─────┘  └─────────┘
typ      └─────┘  └─────────┘
doc      └─────┘  └─────────┘
txt      └─────┘  └─────────┘
par      └─────┘  └─────────┘
pid           └┘           └┘
st   ───┘└─────┘└───────────┘└─
285      apply not_le_of_lt (typein_lt_type r a),
id             └──────────┘  └────────────┘  
src      └────┘└──────────┘ └────────────┘  
typ      └────┘└──────────┘ └────────────┘
doc      └────┘                             
txt      └────┘                             
par      └────┘                             
pid                                        
st   ──────────────────────────────────────────┘└─
286      rw [← e', sup_le],
id             └┘  └────┘
src      └────┘  └┘└────┘
typ      └────┘└┘└┘└────┘
doc      └────┘  └┘      
txt      └────┘  └┘      
par      └────┘  └┘      
pid        └──┘  └┘      
st   ───────────┘└──────┘└──
287      intro i,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ──────────┘└─
288      simp [set.range] at h,
id             └───────┘
src      └────┘└───────┘└────┘
typ      └────┘└───────┘└────┘
doc      └────┘└───────┘└────┘
txt      └────┘         └────┘
par      └────┘         └────┘
pid                   └──┘
st   ────────────────────────┘└─
289      simpa using le_of_lt ((typein_lt_typein r).2 (h _ i rfl)) },
id                   └──────┘   └──────────────┘          └─┘
src      └──────────┘└──────┘  └──────────────┘ └──┘  └─┘ └─┘└─┘
typ      └──────────┘└──────┘  └──────────────┘└──┘ └─┘└─┘└─┘
doc      └──────────┘                           └──┘  └─┘    └─┘
txt      └──────────┘                           └──┘  └─┘    └─┘
par      └──────────┘                           └──┘  └─┘    └─┘
pid           └────┘                           └──┘  └─┘    └┘
st   ─────────────────────────────────────────────────────────────┘└┘
290    { exact λ i, ⟨_, set.mem_range_self i.1⟩ },
id                      └────────────────┘
src      └────┘ └──┘ └─┘└────────────────┘ └──┘
typ      └────┘ └──┘ └─┘└────────────────┘ └──┘
doc      └────┘ └──┘ └─┘                   └──┘
txt      └────┘ └──┘ └─┘                   └──┘
par      └────┘ └──┘ └─┘                   └──┘
pid            └──┘ └─┘                   └─┘
st   ───┘└─────────────────────────────────────┘└┘
291    { intro a, rcases a with ⟨_, i, rfl⟩, exact ⟨⟨i⟩, by simp⟩ }
id                                                  
src      └─────┘  └─────┘ └───────────────┘  └────┘   └─┘  └──┘└┘
typ      └─────┘  └─────┘└───────────────┘  └────┘  └─┘  └──┘└┘
doc      └─────┘  └─────┘ └───────────────┘  └────┘   └─┘  └──┘└┘
txt      └─────┘  └─────┘ └───────────────┘  └────┘   └─┘  └──┘└┘
par      └─────┘  └─────┘ └───────────────┘  └────┘   └─┘  └──┘└┘
pid           └┘         └───────────────┘          └─┘  └────┘
st   ──────────┘└─────────────────────────┘└──────────────┘└───┘└┘└─
292  end
st   ──┘
293  
294  theorem cof_sup_le {ι} (f : ι → ordinal) (H : ∀ i, f i < sup.{u u} f) :
id                                  └─────┘              └─┘       
src                                  └─────┘                 └─┘
typ                                 └─────┘              └─┘       
doc                                  └─────┘                  └─┘
295    cof (sup.{u u} f) ≤ mk ι :=
id     └─┘  └─┘          └┘ 
src    └─┘  └─┘           └┘
typ    └─┘  └─┘          └┘ 
doc    └─┘  └─┘            └┘
296  by simpa using cof_sup_le_lift.{u u} f H
id                  └─────────────┘        
src     └──────────┘└─────────────┘└─────┘  
typ     └──────────┘└─────────────┘└─────┘
doc     └──────────┘               └─────┘  
txt     └──────────┘               └─────┘  
par     └──────────┘               └─────┘  
pid          └────┘               └─────┘  
st     └──────────────────────────────────────
297  
src  
typ  
doc  
txt  
par  
pid  
st   
298  theorem cof_bsup_le_lift {o : ordinal} : ∀ (f : Π a < o, ordinal), (∀ i h, f i h < bsup o f) →
id                                 └─────┘                  └─────┘             └──┘  
src                                └─────┘                   └─────┘                  └──┘
typ                                └─────┘                  └─────┘             └──┘  
doc                                └─────┘                    └─────┘                   └──┘
299    cof (bsup o f) ≤ o.card.lift :=
id     └─┘  └──┘     └───┘└───┘
src    └─┘  └──┘        └───┘└───┘
typ    └─┘  └──┘     └───┘└───┘
doc    └─┘  └──┘         └───┘└───┘
300  induction_on o $ λ α r _ f H,
id   └──────────┘          
src  └──────────┘
typ  └──────────┘          
301  by rw bsup_type; refine cof_sup_le_lift _ _;
id         └───────┘         └─────────────┘
src     └─┘└───────┘  └─────┘└─────────────┘└──┘
typ     └─┘└───────┘  └─────┘└─────────────┘└──┘
doc     └─┘           └─────┘               └──┘
txt     └─┘           └─────┘               └──┘
par     └─┘           └─────┘               └──┘
pid                                       └──┘
st     └──────────────────────────────────────────
302     rw ← bsup_type; intro a; apply H
id           └───────┘
src     └───┘└───────┘  └─────┘  └────┘ 
typ     └───┘└───────┘  └─────┘  └────┘ 
doc     └───┘           └─────┘  └────┘ 
txt     └───┘           └─────┘  └────┘ 
par     └───┘           └─────┘  └────┘ 
pid       └─┘                └┘        
st   ────────────────────────────────────
303  
src  
typ  
doc  
txt  
par  
pid  
st   
304  theorem cof_bsup_le {o : ordinal} : ∀ (f : Π a < o, ordinal), (∀ i h, f i h < bsup.{u u} o f) →
id                            └─────┘                  └─────┘             └──┘        
src                           └─────┘                    └─────┘                  └──┘
typ                           └─────┘                  └─────┘             └──┘        
doc                           └─────┘                    └─────┘                   └──┘
305    cof (bsup.{u u} o f) ≤ o.card :=
id     └─┘  └──┘           └───┘
src    └─┘  └──┘              └───┘
typ    └─┘  └──┘           └───┘
doc    └─┘  └──┘               └───┘
306  induction_on o $ λ α r _ f H,
id   └──────────┘          
src  └──────────┘
typ  └──────────┘          
307  by simpa using cof_bsup_le_lift.{u u} f H
id                  └──────────────┘        
src     └──────────┘└──────────────┘└─────┘  
typ     └──────────┘└──────────────┘└─────┘
doc     └──────────┘                └─────┘  
txt     └──────────┘                └─────┘  
par     └──────────┘                └─────┘  
pid          └────┘                └─────┘  
st     └───────────────────────────────────────
308  
src  
typ  
doc  
txt  
par  
pid  
st   
309  @[simp] theorem cof_univ : cof univ.{u v} = cardinal.univ :=
id                              └─┘ └──┘        └───────────┘
src                             └─┘ └──┘        └───────────┘
typ                             └─┘ └──┘        └───────────┘
doc    └──┘                     └─┘ └──┘         └───────────┘
310  le_antisymm (cof_le_card _) begin
id   └─────────┘  └─────────┘
src  └─────────┘  └─────────┘
typ  └─────────┘  └─────────┘
st                               └─────
311    refine le_of_forall_lt (λ c h, _),
id            └─────────────┘
src    └─────┘└─────────────┘  └──────┘
typ    └─────┘└─────────────┘  └──────┘
doc    └─────┘                 └──────┘
txt    └─────┘                 └──────┘
par    └─────┘                 └──────┘
pid                           └──────┘
st   ──────────────────────────────────┘└─
312    rcases lt_univ'.1 h with ⟨c, rfl⟩,
id            └──────┘   
src    └─────┘└──────┘└─┘ └────────────┘
typ    └─────┘└──────┘└─┘└────────────┘
doc    └─────┘        └─┘ └────────────┘
txt    └─────┘        └─┘ └────────────┘
par    └─────┘        └─┘ └────────────┘
pid                  └─┘ └────────────┘
st   ──────────────────────────────────┘└─
313    rcases @cof_eq ordinal.{u} (<) _ with ⟨S, H, Se⟩,
id             └────┘ └─────┘     
src    └─────┘ └────┘└─────┘└───┘└──────────────────┘
typ    └─────┘ └────┘└─────┘└───┘└──────────────────┘
doc    └─────┘       └─────┘└───┘ └──────────────────┘
txt    └─────┘              └───┘ └──────────────────┘
par    └─────┘              └───┘ └──────────────────┘
pid                        └───┘ └──────────────────┘
st   ─────────────────────────────────────────────────┘└─
314    rw [univ, ← lift_cof, ← cardinal.lift_lift, cardinal.lift_lt, ← Se],
id         └──┘    └──────┘    └────────────────┘  └──────────────┘    └┘
src    └──┘└──┘└──┘└──────┘└──┘└────────────────┘└┘└──────────────┘└──┘  
typ    └──┘└──┘└──┘└──────┘└──┘└────────────────┘└┘└──────────────┘└──┘└┘
doc    └──┘└──┘└──┘        └──┘                  └┘                └──┘  
txt    └──┘    └──┘        └──┘                  └┘                └──┘  
par    └──┘    └──┘        └──┘                  └┘                └──┘  
pid      └┘    └──┘        └──┘                  └┘                └──┘  
st   ─────────┘└──────────┘└────────────────────┘└────────────────┘└────┘└──
315    refine lt_of_not_ge (λ h, _),
id            └──────────┘
src    └─────┘└──────────┘  └────┘
typ    └─────┘└──────────┘  └────┘
doc    └─────┘              └────┘
txt    └─────┘              └────┘
par    └─────┘              └────┘
pid                        └────┘
st   ─────────────────────────────┘└─
316    cases cardinal.lift_down h with a e,
id           └────────────────┘ 
src    └────┘└────────────────┘ └───────┘
typ    └────┘└────────────────┘└───────┘
doc    └────┘                   └───────┘
txt    └────┘                   └───────┘
par    └────┘                   └───────┘
pid                            └───────┘
st   ────────────────────────────────────┘└─
317    refine quotient.induction_on a (λ α e, _) e,
id            └───────────────────┘             
src    └─────┘└───────────────────┘   └───────┘
typ    └─────┘└───────────────────┘  └───────┘
doc    └─────┘                        └───────┘
txt    └─────┘                        └───────┘
par    └─────┘                        └───────┘
pid                                  └───────┘
st   ────────────────────────────────────────────┘└─
318    cases quotient.exact e with f,
id           └────────────┘ 
src    └────┘└────────────┘ └─────┘
typ    └────┘└────────────┘└─────┘
doc    └────┘               └─────┘
txt    └────┘               └─────┘
par    └────┘               └─────┘
pid                        └─────┘
st   ──────────────────────────────┘└─
319    have f := equiv.ulift.symm.trans f,
id               └────────────────────┘ 
src    └────────┘└────────────────────┘
typ    └────────┘└────────────────────┘
doc    └────────┘                      
txt    └────────┘                      
par    └────────┘                      
pid    └────┘└─┘                      
st   ───────────────────────────────────┘└─
320    let g := λ a, (f a).1,
id                    
src    └───────┘ └──┘   └─┘
typ    └───────┘ └──┘  └─┘
doc    └───────┘ └──┘   └─┘
txt    └───────┘ └──┘   └─┘
par    └───────┘ └──┘   └─┘
pid    └───┘└─┘ └──┘   └┘
st   ──────────────────────┘└─
321    let o := succ (sup.{u u} g),
id              └──┘  └─┘       
src    └───────┘└──┘ └─┘└─────┘ 
typ    └───────┘└──┘ └─┘└─────┘
doc    └───────┘└──┘ └─┘└─────┘ 
txt    └───────┘        └─────┘ 
par    └───────┘        └─────┘ 
pid    └───┘└─┘        └─────┘ 
st   ────────────────────────────┘└─
322    rcases H o with ⟨b, h, l⟩,
id             
src    └─────┘  └─────────────┘
typ    └─────┘└─────────────┘
doc    └─────┘  └─────────────┘
txt    └─────┘  └─────────────┘
par    └─────┘  └─────────────┘
pid            └─────────────┘
st   ──────────────────────────┘└─
323    refine l (lt_succ.2 _),
id              └─────┘
src    └─────┘  └─────┘└───┘
typ    └─────┘ └─────┘└───┘
doc    └─────┘         └───┘
txt    └─────┘         └───┘
par    └─────┘         └───┘
pid                   └───┘
st   ───────────────────────┘└─
324    rw ← show g (f.symm ⟨b, h⟩) = b, by dsimp [g]; simp,
id                 └────┘                     
src    └───┘      └────┘  └┘ └─┘ └───┘└─────┘ └┘└──┘
typ    └───┘     └────┘  └┘└─┘└───┘└─────┘└┘└──┘
doc    └───┘              └┘ └─┘  └───┘└─────┘ └┘└──┘
txt    └───┘              └┘ └─┘  └───┘└─────┘ └┘└──┘
par    └───┘              └┘ └─┘  └───┘└─────┘ └┘└──┘
pid      └─┘              └┘ └─┘  └──────────┘ └─────┘
st   ────────────────────────────────────┘└──────────────┘└─
325    apply le_sup
id           └────┘
src    └────┘└────┘
typ    └────┘└────┘
doc    └────┘      
txt    └────┘      
par    └────┘      
pid               
st   ──────────────┘
326  end
st   └─┘
327  
328  theorem sup_lt_ord {ι} (f : ι → ordinal) {c : ordinal} (H1 : cardinal.mk ι < c.cof)
id                                  └─────┘       └─────┘        └─────────┘   └──┘
src                                  └─────┘       └─────┘        └─────────┘     └──┘
typ                                 └─────┘       └─────┘        └─────────┘   └──┘
doc                                  └─────┘       └─────┘        └─────────┘      └──┘
329    (H2 : ∀ i, f i < c) : sup.{u u} f < c :=
id                      └─┘         
src                         └─┘         
typ                     └─┘         
doc                          └─┘
330  begin
st   └─────
331    apply lt_of_le_of_ne,
id           └────────────┘
src    └────┘└────────────┘
typ    └────┘└────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────┘└─
332    { rw [sup_le], exact λ i, le_of_lt (H2 i) },
id           └────┘              └──────┘  └┘
src      └──┘└────┘  └────┘ └──┘└──────┘    └┘
typ      └──┘└────┘  └────┘ └──┘└──────┘ └┘ └┘
doc      └──┘        └────┘ └──┘            └┘
txt      └──┘        └────┘ └──┘            └┘
par      └──┘        └────┘ └──┘            └┘
pid        └┘              └──┘            
st   ───┘└────────┘└────────────────────────────┘└┘
333    rintro h, apply not_le_of_lt H1,
id                     └──────────┘ └┘
src    └──────┘  └────┘└──────────┘
typ    └──────┘  └────┘└──────────┘└┘
doc    └──────┘  └────┘            
txt    └──────┘  └────┘            
par    └──────┘  └────┘            
pid          └┘                   
st   ─────────┘└─────────────────────┘└─
334    simpa [sup_ord, H2, h] using cof_sup_le.{u} f
id            └─────┘  └┘          └────────┘     
src    └─────┘└─────┘└┘  └┘ └──────┘└────────┘└───┘ 
typ    └─────┘└─────┘└┘└┘└┘└──────┘└────────┘└───┘
doc    └─────┘       └┘  └┘ └──────┘          └───┘ 
txt    └─────┘       └┘  └┘ └──────┘          └───┘ 
par    └─────┘       └┘  └┘ └──────┘          └───┘ 
pid                └┘  └┘ └────┘          └───┘ 
st   ───────────────────────────────────────────────┘
335  end
st   └─┘
336  
337  theorem sup_lt {ι} (f : ι → cardinal) {c : cardinal} (H1 : cardinal.mk ι < c.ord.cof)
id                              └──────┘       └──────┘        └─────────┘   └──┘└──┘
src                              └──────┘       └──────┘        └─────────┘     └──┘└──┘
typ                             └──────┘       └──────┘        └─────────┘   └──┘└──┘
doc                              └──────┘       └──────┘        └─────────┘      └──┘└──┘
338    (H2 : ∀ i, f i < c) : cardinal.sup.{u u} f < c :=
id                      └──────────┘         
src                         └──────────┘         
typ                     └──────────┘         
doc                          └──────────┘
339  by { rw [←ord_lt_ord, ←sup_ord], apply sup_lt_ord _ H1, intro i, rw ord_lt_ord, apply H2 }
id             └────────┘   └─────┘         └────────┘   └┘              └────────┘
src       └───┘└────────┘└─┘└─────┘  └────┘└────────┘└─┘    └─────┘  └─┘└────────┘  └────┘  
typ       └───┘└────────┘└─┘└─────┘  └────┘└────────┘└─┘└┘  └─────┘  └─┘└────────┘  └────┘  
doc       └───┘          └─┘         └────┘          └─┘    └─────┘  └─┘            └────┘  
txt       └───┘          └─┘         └────┘          └─┘    └─────┘  └─┘            └────┘  
par       └───┘          └─┘         └────┘          └─┘    └─────┘  └─┘            └────┘  
pid         └─┘          └─┘                        └─┘         └┘                       
st     └────────────────┘└────────┘└──────────────────────┘└───────┘└─────────────┘└─────────┘└┘
340  
341  /-- If the union of s is unbounded and s is smaller than the cofinality, then s has an unbounded member -/
342  theorem unbounded_of_unbounded_sUnion (r : α → α → Prop) [wo : is_well_order α r] {s : set (set α)}
id                                                                └───────────┘         └─┘  └─┘ 
src                                                                 └───────────┘           └─┘  └─┘
typ                                                               └───────────┘         └─┘  └─┘ 
doc                                                                 └───────────┘
343    (h₁ : unbounded r $ ⋃₀ s) (h₂ : mk s < strict_order.cof r) : ∃(x ∈ s), unbounded r x :=
id           └───────┘    └┘         └┘   └──────────────┘           └───────┘  
src          └───────┘     └┘          └┘    └──────────────┘              └───────┘
typ          └───────┘    └┘         └┘   └──────────────┘           └───────┘  
doc          └───────┘                 └┘                                     └───────┘
344  begin
st   └─────
345    by_contra h, simp only [not_exists, exists_prop, not_and, not_unbounded_iff] at h,
id                             └────────┘  └─────────┘  └─────┘  └───────────────┘
src    └─────────┘  └─────────┘└────────┘└┘└─────────┘└┘└─────┘└┘└───────────────┘└────┘
typ    └─────────┘  └─────────┘└────────┘└┘└─────────┘└┘└─────┘└┘└───────────────┘└────┘
doc    └─────────┘  └─────────┘          └┘           └┘       └┘                 └────┘
txt    └─────────┘  └─────────┘          └┘           └┘       └┘                 └────┘
par    └─────────┘  └─────────┘          └┘           └┘       └┘                 └────┘
pid             └┘      └──┘└┘          └┘           └┘       └┘                 └──┘
st   ────────────┘└────────────────────────────────────────────────────────────────────┘└─
346    apply not_le_of_lt h₂,
id           └──────────┘ └┘
src    └────┘└──────────┘
typ    └────┘└──────────┘└┘
doc    └────┘            
txt    └────┘            
par    └────┘            
pid                     
st   ──────────────────────┘└─
347    let f : s → α := λ x : s, wo.wf.sup x (h x.1 x.2),
id                            └───────┘    
src    └──────┘   └──┘ └───┘ └┘└───────┘    └─┘ └─┘
typ    └──────┘ └──┘ └───┘└┘└───────┘   └─┘ └─┘
doc    └──────┘   └──┘ └───┘ └┘             └─┘ └─┘
txt    └──────┘   └──┘ └───┘ └┘             └─┘ └─┘
par    └──────┘   └──┘ └───┘ └┘             └─┘ └─┘
pid    └───┘└─┘   └──┘ └───┘ └┘             └─┘ └─┘
st   ──────────────────────────────────────────────────┘└─
348    let t : set α := range f,
id             └─┘     └───┘ 
src    └──────┘└─┘ └──┘└───┘
typ    └──────┘└─┘└──┘└───┘
doc    └──────┘    └──┘└───┘
txt    └──────┘    └──┘     
par    └──────┘    └──┘     
pid    └───┘└─┘    └──┘     
st   ─────────────────────────┘└─
349    have : mk t ≤ mk s, exact mk_range_le, refine le_trans _ this,
id                 └┘         └─────────┘         └──────┘   └──┘
src    └─────┘   └┘   └────┘└─────────┘  └─────┘└──────┘└─┘
typ    └─────┘  └┘  └────┘└─────────┘  └─────┘└──────┘└─┘└──┘
doc    └─────┘    └┘   └────┘             └─────┘        └─┘
txt    └─────┘         └────┘             └─────┘        └─┘
par    └─────┘         └────┘             └─────┘        └─┘
pid    └───┘└┘                                         └─┘
st   ───────────────────┘└─────────────────┘└──────────────────────┘└─
350    have : unbounded r t,
id            └───────┘  
src    └─────┘└───────┘ 
typ    └─────┘└───────┘
doc    └─────┘└───────┘ 
txt    └─────┘          
par    └─────┘          
pid    └───┘└┘          
st   ─────────────────────┘└─
351    { intro x, rcases h₁ x with ⟨y, ⟨c, hc, hy⟩, hxy⟩,
id                       └┘ 
src      └─────┘  └─────┘   └─────────────────────────┘
typ      └─────┘  └─────┘└┘└─────────────────────────┘
doc      └─────┘  └─────┘   └─────────────────────────┘
txt      └─────┘  └─────┘   └─────────────────────────┘
par      └─────┘  └─────┘   └─────────────────────────┘
pid           └┘           └─────────────────────────┘
st   ───┘└─────┘└──────────────────────────────────────┘└─
352      refine ⟨f ⟨c, hc⟩, mem_range_self _, _⟩, intro hxz, apply hxy,
id                   └┘   └────────────┘
src      └─────┘    └┘  └─┘└────────────┘└────┘  └───────┘  └────┘
typ      └─────┘  └┘└┘└─┘└────────────┘└────┘  └───────┘  └────┘
doc      └─────┘    └┘  └─┘              └────┘  └───────┘  └────┘
txt      └─────┘    └┘  └─┘              └────┘  └───────┘  └────┘
par      └─────┘    └┘  └─┘              └────┘  └───────┘  └────┘
pid                └┘  └─┘              └────┘       └──┘       
st   ──────────────────────────────────────────┘└─────────┘└─────────┘└─
353      refine trans (wo.wf.lt_sup _ hy) hxz },
id              └───┘  └──────────┘   └┘  └─┘
src      └─────┘└───┘ └──────────┘└─┘  └┘   
typ      └─────┘└───┘ └──────────┘└─┘└┘└┘└─┘
doc      └─────┘                  └─┘  └┘   
txt      └─────┘                  └─┘  └┘   
par      └─────┘                  └─┘  └┘   
pid                              └─┘  └┘   
st   ────────────────────────────────────────┘└┘
354    exact cardinal.min_le _ (subtype.mk t this)
id           └─────────────┘    └────────┘  └──┘
src    └────┘└─────────────┘└─┘ └────────┘     └┘
typ    └────┘└─────────────┘└─┘ └────────┘└──┘└┘
doc    └────┘               └─┘                └┘
txt    └────┘               └─┘                └┘
par    └────┘               └─┘                └┘
pid                        └─┘                
st   ─────────────────────────────────────────────┘
355  end
st   └─┘
356  
357  /-- If the union of s is unbounded and s is smaller than the cofinality, then s has an unbounded member -/
358  theorem unbounded_of_unbounded_Union {α β : Type u} (r : α → α → Prop) [wo : is_well_order α r]
id                                                                              └───────────┘  
src                                                                               └───────────┘
typ                                                                             └───────────┘  
doc                                                                               └───────────┘
359    (s : β → set α)
id             └─┘ 
src             └─┘
typ            └─┘ 
360    (h₁ : unbounded r $ ⋃x, s x) (h₂ : mk β < strict_order.cof r) : ∃x : β, unbounded r (s x) :=
id           └───────┘              └┘   └──────────────┘          └───────┘    
src          └───────┘                  └┘    └──────────────┘            └───────┘
typ          └───────┘              └┘   └──────────────┘          └───────┘    
doc          └───────┘                  └┘                                   └───────┘
361  begin
st   └─────
362    rw [← sUnion_range] at h₁,
id           └──────────┘
src    └────┘└──────────┘└─────┘
typ    └────┘└──────────┘└─────┘
doc    └────┘            └─────┘
txt    └────┘            └─────┘
par    └────┘            └─────┘
pid      └──┘            └────┘
st   ───────────────────┘└────┘└─
363    have : mk ↥(range (λ (i : β), s i)) < strict_order.cof r := lt_of_le_of_lt mk_range_le h₂,
id            └┘  └───┘                  └──────────────┘     └────────────┘ └─────────┘ └┘
src    └─────┘└┘ └───┘  └────┘ └─┘  └─┘└──────────────┘ └──┘└────────────┘└─────────┘
typ    └─────┘└┘ └───┘  └────┘└─┘ └─┘└──────────────┘└──┘└────────────┘└─────────┘└┘
doc    └─────┘└┘  └───┘  └────┘ └─┘  └─┘                  └──┘                         
txt    └─────┘           └────┘ └─┘  └─┘                  └──┘                         
par    └─────┘           └────┘ └─┘  └─┘                  └──┘                         
pid    └───┘└┘           └────┘ └─┘  └─┘                  └──┘                         
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
364    rcases unbounded_of_unbounded_sUnion r h₁ this with ⟨_, ⟨x, rfl⟩, u⟩, exact ⟨x, u⟩
id            └───────────────────────────┘  └┘ └──┘                                 
src    └─────┘└───────────────────────────┘       └────────────────────┘  └────┘  └┘ └┘
typ    └─────┘└───────────────────────────┘└┘└──┘└────────────────────┘  └────┘ └┘└┘
doc    └─────┘└───────────────────────────┘       └────────────────────┘  └────┘  └┘ └┘
txt    └─────┘                                    └────────────────────┘  └────┘  └┘ └┘
par    └─────┘                                    └────────────────────┘  └────┘  └┘ └┘
pid                                              └────────────────────┘         └┘ 
st   ─────────────────────────────────────────────────────────────────────┘└─────────────┘
365  end
st   └─┘
366  
367  /-- The infinite pigeonhole principle-/
368  theorem infinite_pigeonhole {β α : Type u} (f : β → α) (h₁ : cardinal.omega ≤ mk β)
id                                                              └────────────┘  └┘ 
src                                                               └────────────┘  └┘
typ                                                             └────────────┘  └┘ 
doc                                                               └────────────┘   └┘
369    (h₂ : mk α < (mk β).ord.cof) : ∃a : α, mk (f ⁻¹' {a}) = mk β :=
id           └┘    └┘  └─┘ └─┘          └┘   └─┘     └┘ 
src          └┘     └┘   └─┘ └─┘           └┘    └─┘      └┘
typ          └┘    └┘  └─┘ └─┘          └┘   └─┘     └┘ 
doc          └┘      └┘   └─┘ └─┘             └┘    └─┘        └┘
370  begin
st   └─────
371    have : ¬∀a, mk (f ⁻¹' {a}) < mk β,
id                     └─┘      └┘ 
src    └─────┘      └─┘└──┘└┘
typ    └─────┘     └─┘└──┘└┘
doc    └─────┘       └─┘ └──┘ └┘
txt    └─────┘           └──┘   
par    └─────┘           └──┘   
pid    └───┘└┘           └──┘   
st   ──────────────────────────────────┘└─
372    { intro h,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ───┘└─────┘└─
373      apply not_lt_of_ge (ge_of_eq $ mk_univ),
id             └──────────┘  └──────┘   └─────┘
src      └────┘└──────────┘ └──────┘ └─────┘
typ      └────┘└──────────┘ └──────┘ └─────┘
doc      └────┘                             
txt      └────┘                             
par      └────┘                             
pid                                        
st   ──────────────────────────────────────────┘└─
374      rw [←@preimage_univ _ _ f, ←Union_of_singleton, preimage_Union],
id             └───────────┘        └────────────────┘  └────────────┘
src      └───┘ └───────────┘└───┘ └─┘└────────────────┘└┘└────────────┘
typ      └───┘ └───────────┘└───┘└─┘└────────────────┘└┘└────────────┘
doc      └───┘              └───┘ └─┘                  └┘              
txt      └───┘              └───┘ └─┘                  └┘              
par      └───┘              └───┘ └─┘                  └┘              
pid        └─┘              └───┘ └─┘                  └┘              
st   ────────────────────────────┘└───────────────────┘└──────────────┘└──
375      apply lt_of_le_of_lt mk_Union_le_sum_mk,
id             └────────────┘ └────────────────┘
src      └────┘└────────────┘└────────────────┘
typ      └────┘└────────────┘└────────────────┘
doc      └────┘              
txt      └────┘              
par      └────┘              
pid                         
st   ──────────────────────────────────────────┘└─
376      apply lt_of_le_of_lt (sum_le_sup _),
id             └────────────┘  └────────┘
src      └────┘└────────────┘ └────────┘└─┘
typ      └────┘└────────────┘ └────────┘└─┘
doc      └────┘                         └─┘
txt      └────┘                         └─┘
par      └────┘                         └─┘
pid                                    └─┘
st   ──────────────────────────────────────┘└─
377      apply mul_lt_of_lt h₁ (lt_of_lt_of_le h₂ $ cof_ord_le _),
id             └──────────┘ └┘  └────────────┘ └┘   └────────┘
src      └────┘└──────────┘   └────────────┘   └────────┘└─┘
typ      └────┘└──────────┘└┘ └────────────┘└┘ └────────┘└─┘
doc      └────┘                                          └─┘
txt      └────┘                                          └─┘
par      └────┘                                          └─┘
pid                                                     └─┘
st   ───────────────────────────────────────────────────────────┘└─
378      exact sup_lt _ h₂ h },
id             └────┘   └┘ 
src      └────┘└────┘└─┘   
typ      └────┘└────┘└─┘└┘
doc      └────┘      └─┘   
txt      └────┘      └─┘   
par      └────┘      └─┘   
pid                 └─┘   
st   ───────────────────────┘└┘
379    rw [not_forall] at this, cases this with x h,
id         └────────┘                 └──┘
src    └──┘└────────┘└───────┘  └────┘    └───────┘
typ    └──┘└────────┘└───────┘  └────┘└──┘└───────┘
doc    └──┘          └───────┘  └────┘    └───────┘
txt    └──┘          └───────┘  └────┘    └───────┘
par    └──┘          └───────┘  └────┘    └───────┘
pid      └┘          └──────┘           └───────┘
st   ───────────────┘└──────┘└───────────────────┘└─
380    use x, apply le_antisymm _ (le_of_not_gt h),
id                 └─────────┘    └──────────┘ 
src    └──┘   └────┘└─────────┘└─┘ └──────────┘ 
typ    └──┘  └────┘└─────────┘└─┘ └──────────┘
doc    └──┘   └────┘           └─┘              
txt    └──┘   └────┘           └─┘              
par    └──┘   └────┘           └─┘              
pid                          └─┘              
st   ──────┘└────────────────────────────────────┘└─
381    rw [le_mk_iff_exists_set], exact ⟨_, rfl⟩
id         └──────────────────┘             └─┘
src    └──┘└──────────────────┘  └────┘ └─┘└─┘└┘
typ    └──┘└──────────────────┘  └────┘ └─┘└─┘└┘
doc    └──┘                      └────┘ └─┘   └┘
txt    └──┘                      └────┘ └─┘   └┘
par    └──┘                      └────┘ └─┘   └┘
pid      └┘                            └─┘   
st   ─────────────────────────┘└────────────────┘
382  end
st   └─┘
383  
384  /-- pigeonhole principle for a cardinality below the cardinality of the domain -/
385  theorem infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : cardinal) (hθ : θ ≤ mk β)
id                                                                  └──────┘          └┘ 
src                                                                   └──────┘           └┘
typ                                                                 └──────┘          └┘ 
doc                                                                   └──────┘            └┘
386    (h₁ : cardinal.omega ≤ θ) (h₂ : mk α < θ.ord.cof) : ∃a : α, θ ≤ mk (f ⁻¹' {a}) :=
id           └────────────┘          └┘   └──┘└──┘           └┘   └─┘ 
src          └────────────┘           └┘     └──┘└──┘             └┘    └─┘ 
typ          └────────────┘          └┘   └──┘└──┘           └┘   └─┘ 
doc          └────────────┘            └┘      └──┘└──┘                └┘    └─┘
387  begin
st   └─────
388    rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩,
id            └──────────────────┘   └┘
src    └─────┘└──────────────────┘└─┘  └────────────┘
typ    └─────┘└──────────────────┘└─┘└┘└────────────┘
doc    └─────┘                    └─┘  └────────────┘
txt    └─────┘                    └─┘  └────────────┘
par    └─────┘                    └─┘  └────────────┘
pid                              └─┘  └────────────┘
st   ───────────────────────────────────────────────┘└─
389    cases infinite_pigeonhole (f ∘ subtype.val : s → α) h₁ h₂ with a ha,
id           └─────────────────┘    └─────────┘        └┘ └┘
src    └────┘└─────────────────┘  └─────────┘└─┘   └┘    └────────┘
typ    └────┘└─────────────────┘ └─────────┘└─┘ └┘└┘└┘└────────┘
doc    └────┘└─────────────────┘              └─┘   └┘    └────────┘
txt    └────┘                                 └─┘   └┘    └────────┘
par    └────┘                                 └─┘   └┘    └────────┘
pid                                          └─┘   └┘    └────────┘
st   ────────────────────────────────────────────────────────────────────┘└─
390    use a, rw [←ha, @preimage_comp _ _ _ subtype.val f],
id                └┘   └───────────┘       └─────────┘ 
src    └──┘   └───┘  └┘ └───────────┘└─────┘└─────────┘ 
typ    └──┘  └───┘└┘└┘ └───────────┘└─────┘└─────────┘
doc    └──┘   └───┘  └┘              └─────┘            
txt    └──┘   └───┘  └┘              └─────┘            
par    └──┘   └───┘  └┘              └─────┘            
pid            └─┘  └┘              └─────┘            
st   ──────┘└───────┘└──────────────────────────────────┘└──
391    apply mk_preimage_of_injective _ _ subtype.val_injective
id           └──────────────────────┘     └───────────────────┘
src    └────┘└──────────────────────┘└───┘└───────────────────┘
typ    └────┘└──────────────────────┘└───┘└───────────────────┘
doc    └────┘                        └───┘                     
txt    └────┘                        └───┘                     
par    └────┘                        └───┘                     
pid                                 └───┘                     
st   ──────────────────────────────────────────────────────────┘
392  end
st   └─┘
393  
394  theorem infinite_pigeonhole_set {β α : Type u} {s : set β} (f : s → α) (θ : cardinal)
id                                                       └─┘                  └──────┘
src                                                      └─┘                     └──────┘
typ                                                      └─┘                  └──────┘
doc                                                                              └──────┘
395    (hθ : θ ≤ mk s) (h₁ : cardinal.omega ≤ θ) (h₂ : mk α < θ.ord.cof) :
id             └┘         └────────────┘          └┘   └──┘└──┘
src             └┘          └────────────┘           └┘     └──┘└──┘
typ            └┘         └────────────┘          └┘   └──┘└──┘
doc              └┘          └────────────┘            └┘      └──┘└──┘
396      ∃(a : α) (t : set β) (h : t ⊆ s), θ ≤ mk t ∧ ∀{{x}} (hx : x ∈ t), f ⟨x, h hx⟩ = a :=
id                   └─┘              └┘                         └┘   
src                   └─┘                  └┘                                    
typ                  └─┘              └┘                         └┘   
doc                                            └┘
397  begin
st   └─────
398    cases infinite_pigeonhole_card f θ hθ h₁ h₂ with a ha,
id           └──────────────────────┘   └┘ └┘ └┘
src    └────┘└──────────────────────┘        └────────┘
typ    └────┘└──────────────────────┘└┘└┘└┘└────────┘
doc    └────┘└──────────────────────┘        └────────┘
txt    └────┘                                └────────┘
par    └────┘                                └────────┘
pid                                         └────────┘
st   ──────────────────────────────────────────────────────┘└─
399    refine ⟨a, {x | ∃(h : x ∈ s), f ⟨x, h⟩ = a}, _, _, _⟩,
id                                       
src    └─────┘  └┘└──┘└───┘     └┘ └┘ └─────────┘
typ    └─────┘  └┘└──┘└───┘   └┘ └┘└─────────┘
doc    └─────┘  └┘ └──┘ └───┘       └┘ └┘  └─────────┘
txt    └─────┘  └┘ └──┘ └───┘       └┘ └┘  └─────────┘
par    └─────┘  └┘ └──┘ └───┘       └┘ └┘  └─────────┘
pid            └┘ └──┘ └───┘       └┘ └┘  └─────────┘
st   ──────────────────────────────────────────────────────┘└─
400    { rintro x ⟨hx, hx'⟩, exact hx },
id                                 └┘
src      └────────────────┘  └────┘  
typ      └────────────────┘  └────┘└┘
doc      └────────────────┘  └────┘  
txt      └────────────────┘  └────┘  
par      └────────────────┘  └────┘  
pid            └──────────┘         
st   ───┘└────────────────┘└─────────┘└┘
401    { refine le_trans ha _, apply ge_of_eq, apply quotient.sound, constructor,
id              └──────┘ └┘          └──────┘        └────────────┘
src      └─────┘└──────┘  └┘  └────┘└──────┘  └────┘└────────────┘  └─────────┘
typ      └─────┘└──────┘└┘└┘  └────┘└──────┘  └────┘└────────────┘  └─────────┘
doc      └─────┘          └┘  └────┘          └────┘                └─────────┘
txt      └─────┘          └┘  └────┘          └────┘                └─────────┘
par      └─────┘          └┘  └────┘          └────┘                └─────────┘
pid                      └┘                      
st   ───┘└──────────────────┘└──────────────┘└────────────────────┘└───────────┘└─
402      refine equiv.trans _ (equiv.subtype_subtype_equiv_subtype_exists _ _).symm,
id              └─────────┘    └────────────────────────────────────────┘
src      └─────┘└─────────┘└─┘ └────────────────────────────────────────┘└────────┘
typ      └─────┘└─────────┘└─┘ └────────────────────────────────────────┘└────────┘
doc      └─────┘           └─┘                                           └────────┘
txt      └─────┘           └─┘                                           └────────┘
par      └─────┘           └─┘                                           └────────┘
pid                       └─┘                                           └───────┘
st   ─────────────────────────────────────────────────────────────────────────────┘└┘
403      simp only [set_coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_set_of_eq] },
st                                                                                      └┘
404    rintro x ⟨hx, hx'⟩, exact hx'
405  end
st   └─┘
406  
407  end ordinal
408  
409  namespace cardinal
410  open ordinal
411  
412  local infixr ^ := @pow cardinal.{u} cardinal cardinal.has_pow
id                          └──────┘       └────┘   └┘  └┘  └┘  └┘
src                         └──────┘       └────┘   └┘  └┘  └┘  └┘
typ                         └──────┘       └────┘   └┘  └┘  └┘  └┘
doc                         └──────┘       └────┘
413  
414  /-- A cardinal is a limit if it is not zero or a successor
415    cardinal. Note that `ω` is a limit cardinal by this definition. -/
416  def is_limit (c : cardinal) : Prop :=
id                     └┘  └──┘
src                    └┘  └──┘
typ                    └┘  └──┘
doc                    └┘  └──┘
417  c ≠ 0 ∧ ∀ x < c, succ x < c
id                          
src        
typ                         
418  
419  /-- A cardinal is a strong limit if it is not zero and it is
420    closed under powersets. Note that `ω` is a strong limit by this definition. -/
421  def is_strong_limit (c : cardinal) : Prop :=
id                             └┘ └┘
src                            └┘ └┘
typ                            └┘ └┘
doc                            └┘ └┘
422  c ≠ 0 ∧ ∀ x < c, 2 ^ x < c
id                        
src        
typ                       
423  
424  theorem is_strong_limit.is_limit {c} (H : is_strong_limit c) : is_limit c :=
id                                               └┘  └┘  └┘       └┘  └┘   
src                                              └┘  └┘  └┘        └┘  └┘
typ                                              └┘  └┘  └┘       └┘  └┘   
doc                                              └┘  └┘  └┘        └┘  └┘
425  ⟨H.1, λ x h, lt_of_le_of_lt (succ_le.2 $ cantor _) (H.2 _ h)⟩
id                                                     
typ                                                    
426  
427  /-- A cardinal is regular if it is infinite and it equals its own cofinality. -/
428  def is_regular (c : cardinal) : Prop :=
id                         └──┘
src                        └──┘
typ                        └──┘
doc                        └──┘
429  omega ≤ c ∧ c.ord.cof = c
id   └───┘       └┘  └┘   
src  └───┘         └┘  └┘
typ  └───┘       └┘  └┘   
doc  └───┘          └┘  └┘
430  
431  theorem cof_is_regular {o : ordinal} (h : o.is_limit) : is_regular o.cof :=
id                                └┘ └┘        └┘ └┘ └┘      └┘  └┘     
src                               └┘ └┘         └┘ └┘ └┘      └┘  └┘      
typ                               └┘ └┘        └┘ └┘ └┘      └┘  └┘     
doc                               └┘ └┘         └┘ └┘ └┘      └┘  └┘      
432  ⟨omega_le_cof.2 h, cof_cof _⟩
id                   
typ                  
433  
434  theorem omega_is_regular : is_regular omega :=
id                                └┘  └┘  └───┘
src                               └┘  └┘  └───┘
typ                               └┘  └┘  └───┘
doc                               └┘  └┘  └───┘
435  ⟨le_refl _, by simp⟩
436  
437  theorem succ_is_regular {c : cardinal.{u}} (h : omega ≤ c) : is_regular (succ c) :=
id                                └──┘  └┘           └──┘         └┘  └┘  └┘
src                               └──┘  └┘           └──┘         └┘  └┘  └┘
typ                               └──┘  └┘           └──┘         └┘  └┘  └┘
doc                               └──┘  └┘           └──┘         └┘  └┘  └┘
438  ⟨le_trans h (le_of_lt $ lt_succ_self _), begin
439    refine le_antisymm (cof_ord_le _) (succ_le.2 _),
440    cases quotient.exists_rep (succ c) with α αe, simp at αe,
id                                └──┘ 
src                               └──┘
typ                               └──┘ 
doc                               └──┘
441    rcases ord_eq α with ⟨r, wo, re⟩, resetI,
id                   
typ                  
442    have := ord_is_limit (le_trans h $ le_of_lt $ lt_succ_self _),
443    rw [← αe, re] at this ⊢,
444    rcases cof_eq' r this with ⟨S, H, Se⟩,
id                     └──┘
typ                    └──┘
445    rw [← Se],
446    apply lt_imp_lt_of_le_imp_le (mul_le_mul_right c),
id                                                    
typ                                                   
447    rw [mul_eq_self h, ← succ_le, ← αe, ← sum_const],
448    refine le_trans _ (sum_le_sum (λ x:S, card (typein r x)) _ _),
id                                           └──┘         
src                                          └──┘
typ                                          └──┘         
doc                                          └──┘
449    { simp [typein, sum_mk (λ x:S, {a//r a x})],
id                                       
typ                                      
450      refine ⟨embedding.of_surjective _⟩,
451      { exact λ x, x.2.1 },
st                          └┘
452      { exact λ a, let ⟨b, h, ab⟩ := H a in ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩ } },
id                              └┘
typ                             └┘
st                                                                    └──┘
453    { intro i,
454      rw [← lt_succ, ← lt_ord, ← αe, re],
455      apply typein_lt_type }
st                            └─
456  end⟩
st   ──┘
457  
458  theorem sup_lt_ord_of_is_regular {ι} (f : ι → ordinal)
id                                                └┘  └─┘
src                                                └┘  └─┘
typ                                               └┘  └─┘
doc                                                └┘  └─┘
459    {c} (hc : is_regular c) (H1 : cardinal.mk ι < c)
id                └┘  └┘            └┘  └┘  └┘     
src               └┘  └┘             └┘  └┘  └┘
typ               └┘  └┘            └┘  └┘  └┘     
doc               └┘  └┘             └┘  └┘  └┘
460    (H2 : ∀ i, f i < c.ord) : ordinal.sup.{u u} f < c.ord :=
id                   └─┘                           └┘
src                      └─┘                             └┘
typ                  └─┘                           └┘
doc                      └─┘                             └┘
461  by { apply sup_lt_ord _ _ H2, rw [hc.2], exact H1 }
st                                                     └┘
462  
463  theorem sup_lt_of_is_regular {ι} (f : ι → cardinal)
id                                            └┘  └──┘
src                                            └┘  └──┘
typ                                           └┘  └──┘
doc                                            └┘  └──┘
464    {c} (hc : is_regular c) (H1 : cardinal.mk ι < c)
id               └┘  └┘  └┘          └┘  └┘  └┘     
src              └┘  └┘  └┘           └┘  └┘  └┘
typ              └┘  └┘  └┘          └┘  └┘  └┘     
doc              └┘  └┘  └┘           └┘  └┘  └┘
465    (H2 : ∀ i, f i < c) : sup.{u u} f < c :=
id                                    
typ                                   
466  by { apply sup_lt _ _ H2, rwa [hc.2] }
st                                        └┘
467  
468  theorem sum_lt_of_is_regular {ι} (f : ι → cardinal)
id                                            └┘  └──┘
src                                            └┘  └──┘
typ                                           └┘  └──┘
doc                                            └┘  └──┘
469    {c} (hc : is_regular c) (H1 : cardinal.mk ι < c)
id               └┘  └┘  └┘          └┘  └┘  └┘     
src              └┘  └┘  └┘           └┘  └┘  └┘
typ              └┘  └┘  └┘          └┘  └┘  └┘     
doc              └┘  └┘  └┘           └┘  └┘  └┘
470    (H2 : ∀ i, f i < c) : sum.{u u} f < c :=
id                                    
typ                                   
471  lt_of_le_of_lt (sum_le_sup _) $ mul_lt_of_lt hc.1 H1 $
id                                                └┘
typ                                               └┘
472  sup_lt_of_is_regular f hc H1 H2
id                         └┘
typ                        └┘
473  
474  /-- A cardinal is inaccessible if it is an
475    uncountable regular strong limit cardinal. -/
476  def is_inaccessible (c : cardinal) :=
id                            └┘ └┘ └┘
src                           └┘ └┘ └┘
typ                           └┘ └┘ └┘
doc                           └┘ └┘ └┘
477  omega < c ∧ is_regular c ∧ is_strong_limit c
id    └┘        └┘  └┘      └┘  └┘  └┘  └┘ 
src   └┘         └┘  └┘       └┘  └┘  └┘  └┘
typ   └┘        └┘  └┘      └┘  └┘  └┘  └┘ 
doc   └┘          └┘  └┘        └┘  └┘  └┘  └┘
478  
479  theorem is_inaccessible.mk {c}
480   (h₁ : omega < c) (h₂ : c ≤ c.ord.cof) (h₃ : ∀ x < c, 2 ^ x < c) :
id          └───┘              └┘  └┘                         
src         └───┘                 └┘  └┘
typ         └───┘              └┘  └┘                         
doc         └───┘                 └┘  └┘
481   is_inaccessible c :=
id      └──┘  └──┘   
src     └──┘  └──┘  
typ     └──┘  └──┘   
doc     └──┘  └──┘  
482  ⟨h₁, ⟨le_of_lt h₁, le_antisymm (cof_ord_le _) h₂⟩,
483    ne_of_gt (lt_trans omega_pos h₁), h₃⟩
484  
485  /- Lean's foundations prove the existence of ω many inaccessible
486     cardinals -/
487  theorem univ_inaccessible : is_inaccessible (univ.{u v}) :=
488  is_inaccessible.mk
489    (by simpa using lift_lt_univ' omega)
id                                   └───┘
src                                  └───┘
typ                                  └───┘
doc                                  └───┘
490    (by simp)
491    (λ c h, begin
id        
typ       
492      rcases lt_univ'.1 h with ⟨c, rfl⟩,
493      rw ← lift_two_power.{u (max (u+1) v)},
494      apply lift_lt_univ'
495    end)
st     └─┘
496  
497  theorem lt_power_cof {c : cardinal.{u}} : omega ≤ c → c < c ^ cof c.ord :=
id                             └──┘  └┘        └──┘                   └┘
src                            └──┘  └┘        └──┘                     └┘
typ                            └──┘  └┘        └──┘                   └┘
doc                            └──┘  └┘        └──┘                     └┘
498  quotient.induction_on c $ λ α h, begin
id                              
typ                             
499    rcases ord_eq α with ⟨r, wo, re⟩, resetI,
id                   
typ                  
500    have := ord_is_limit h,
501    rw [mk_def, re] at this ⊢,
502    rcases cof_eq' r this with ⟨S, H, Se⟩,
id                     └──┘
typ                    └──┘
503    have := sum_lt_prod (λ a:S, mk {x // r x a}) (λ _, mk α) (λ i, _),
id                                                      └┘ 
src                                                       └┘
typ                                                     └┘ 
doc                                                       └┘
504    { simp [Se.symm] at this ⊢,
505      refine lt_of_le_of_lt _ this,
506      refine ⟨embedding.of_surjective _⟩,
507      { exact λ x, x.2.1 },
st                          └┘
508      { exact λ a, let ⟨b, h, ab⟩ := H a in ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩ } },
id                              └┘
typ                             └┘
st                                                                    └──┘
509    { have := typein_lt_type r i,
id                              
typ                             
510      rwa [← re, lt_ord] at this }
st                                  └─
511  end
st   ──┘
512  
513  theorem lt_cof_power {a b : cardinal} (ha : omega ≤ a) (b1 : 1 < b) :
id                               └┘  └┘          └───┘               
src                              └┘  └┘          └───┘
typ                              └┘  └┘          └───┘               
doc                              └┘  └┘          └───┘
514    a < cof (b ^ a).ord :=
id                 └┘
src                   └┘
typ                └┘
doc                   └┘
515  begin
516    have b0 : b ≠ 0 := ne_of_gt (lt_trans zero_lt_one b1),
id               
typ              
517    apply lt_imp_lt_of_le_imp_le (power_le_power_left $ power_ne_zero a b0),
id                                                                       
typ                                                                      
518    rw [power_mul, mul_eq_self ha],
519    exact lt_power_cof (le_trans ha $ le_of_lt $ cantor' _ b1),
520  end
st   └─┘
521  
522  end cardinal